Sequences: two schools of thought?

[paurkedal]

@paurkedal

(It would be possible to use phantom types to eliminate these cases, though this is a bit more type engineering than we’re use to from the standard library, and may still require -> . cases when pattern matching.)

Correction: Defining a more generic sequence type is quite straight forward:

type ('a, 's) seq = unit -> ('a, 's) node
and ('a, 's) node =
  | Cont of 'a * ('a, 's) seq
  | Stop of 's

Assuming also

type counit = |

which allows us to eliminate the Stop branch, we have

type 'a infinite_seq = ('a, counit) seq
type 'a finite_seq = ('a, unit) seq

We can also split the Stop branch into “nil” and “error” with the result type and Cont into “cons” and “yield” with the option type:

type ('a, 'e) seq_with_error = ('a, (unit, 'e) result) seq
type ('a, 'e) seq_with_yield_and_error = ('a option, (unit, 'e) result) seq

Lost opportunity or over-engineering?

[silene]

@benjamin-thomas

Even after playing with it for a while, the Seq module doesn’t feel as nice in comparaison, more complicated.

That is true, but note that your original code contains a “bug”, while the version based on Seq does not. The issue is that you are computing one extra prime. (You can plug a counter inside the sieving functions in order to check that your version is performing way more modulos than the Seq-based one.) You can workaround the issue by slightly modifying your ltake function and then propagating the changes:

let rec ltake n l =
  if n > 0 then
    let (Cons (h, tf)) = l () in
    h :: ltake (n - 1) tf
  else
    []

But once fixed, the code is slightly uglier and no longer that clear a winner over the Seq-based one.

[octachron]

Type systems can definitively track evaluation strategy, after all we have lazy in OCaml. Some languages (at least ALGOL, C++) have different kinds of function argument for specifying the evaluation strategy for the argument, this is another evaluation strategy concern in type theory. Linear type systems and variants are also definitively concerned with evaluation strategy since the evaluation strategy can change the number of times a function is evaluated.

[benjamin-thomas]

@mobileink

Shouldn’t that be: because the list has no beginning. Nil is the base case?

I was actually quoting the book here, but it makes sens to me, if we think about the LISP heritage, nil is at the end.

(cons 1 (cons 2 (cons 3 NIL)))

What I like about the infinite type, is that we are describing a property so we could also argue that there is no beginning (really), at least some times.

@lukstafi

Are OCaml datatypes coinductive, or in-between inductive and coinductive?
What is coinduction? - Computer Science Stack Exchange

Is there an aleph_1 sized list?

Interesting. I gather we can express both concepts but my understanding is limited.

I also think I understand this would represent an aleph_0 sized list.

le nats = Seq.ints 0;;

And the following could, in theory, represent an aleph_1 sized list:

let wat = Seq.floats 0.0 (* this does not exist *)

But then we wouldn’t know how to iterate over such a structure (it’s uncountably infinite). Please ignore me if that’s nonsense

@yawaramin

Yes they do, which is why they include the Nil (end of stream) case which one might think is not needed if a stream could never end. So Seq has a more general design than ‘only infinite stream’.

@paurkedal

On the other hand, the Nil is redundant for infinite sequences. While it is possible to use such a sequence type for finite sequences by using an option type for the values, I think this is inelegant, since it does not guarantee that the sequence does not restart after an arbitrary number of None.

Good points, thank you. So if think I was conflating lazy evaluation vs infinity. One may not imply the other.

I understand better now that by having Nil, the producer can decide when the stream ends whereas without it, it would solely be the consumer’s responsibility, so a design choice.

@mobileink

You can use Seq without Nil if you change your method of producing primes.

Yes, I was not really thinking in terms of absolutes, more that I felt thinking about Nil changes one’s way of thinking about things.

This also works, and stays functional if that’s a goal.

let primes =
  let is_prime n =
    let rec check i = i > n / 2 || (n mod i <> 0 && check (i + 1)) in
    check 2
  in
  Seq.filter is_prime (Seq.ints 2)
;;

let () = Seq.iter (printf "%d ") @@ Seq.take 9 primes

@silene

That is true, but note that your original code contains a “bug”, while the version based on Seq does not. The issue is that you are computing one extra prime.

This looks like a great catch, thanks I’ll take a good look at this

---

Overall, I think I understand the Seq module better now, but I’m still fascinated by the simpler construct.

Here’s my latest observation, maybe someone finds that interesting.

I was thinking how to define unfold which generates items.

let rec unfold f x =
  let (h, h') = f x in
  Cons (h, fun () -> unfold f h')
;;

What about a stream if ints?

let ints = unfold (fun n -> (n, n + 1))

This pattern reminds me of the state monad

And one last one, just for fun:

let fibs = unfold (fun (a, b) -> (a, (b, a + b))) (0, 1)

utop # ltake 15 fibs;;
- : int list = [0; 1; 1; 2; 3; 5; 8; 13; 21; 34; 55; 89; 144; 233; 377]

The Seq module equivalent would be:

let fibs = Seq.unfold (fun (a, b) -> Some (a, (b, a + b))) (0, 1)

[mobileink]

@octachron

Type systems can definitively track evaluation strategy, after all we have lazy in OCaml.

Sure, but what is lazy? It’s literally “special”, i.e. not a type in the OCaml type system. It’s a deus ex machina.

I did a little googling and have not found any type theory stuff that mentions evaluation strategy. I think that’s a purely pragmatic issue in PL design. Even in lambda calculus: expression e reduces to e’, that’s all. No need to introduce evaluation strategy unless you’re implementing a PL.

[yawaramin]

Only the syntax sugar is special. You can implement lazy values yourself:

type 'a lazier = {
  mutable result : 'a option;
  thunk : unit -> 'a;
}

let make thunk = {
  result = None;
  thunk;
}

let rec force lazier =
  match lazier.result with
  | None ->
    lazier.result <- Some (lazier.thunk ());
    force lazier
  | Some r -> r

[mobileink]

@yawaramin

Only the syntax sugar is special. You can implement lazy values yourself

Sure, you can do same in C. But the manual explicitly states that lazy is special.

My point being just that this is an interesting point at the intersection of type theory and practical language design.

[yawaramin]

Reference for ‘manual says lazy is special’?

Anyway, I was just responding to

@mobileink

not a type in the OCaml type system

Only the implementation is specialized for performance reasons. Conceptually laziness can be represented just as well as any other type.

[mobileink]

@yawaramin

Reference for ‘manual says lazy is special’?

“The special expression syntax lazy (expr)…”. In the section on module Lazy.

Ok, “special expression syntax” does not necessarily imply that “lazy” is special. But I guess I have not made myself clear so let me try again: how can the definition of a type T say anything about how it’s “values” are evaluated? If foo is a ctor of type T, that’s all there is to say. If function f has type V → T, I cannot see how that has any connection with evaluation strategy. It’s just a fact.

Howsabout this: type theory is science, evaluation strategy is engineering?

[yawaramin]

Fair enough, but types are constructed nominally and used for semantically specialized use cases, this is not unique to OCaml. See eg Rust Send and Sync marker traits, these are placed on types to indicate their thread safety properties, but they don’t inherently mean anything to do with multithreading. They could be called ‘Broadcast’ and ‘Concur’, for example, and their usage would remain the same.

[Frederic_Loyer]

Without the lazy keyword, we could have:

type 'a t = Const of 'a | Fun of (unit -> 'a)
type 'a l = 'a t ref
let lazy' f : 'a l = ref (Fun f)
let force' l = match !l with Const x -> x |  Fun f -> let x = f() in l:= Const x; x

Then lazy ... could appear as a syntactic sugar for lazy' (() -> ...).

Then, sure, the Lazy module manual says it it special, but it is special because of a lazy keyword built in the language (like list are special because of the [...] notation).

There is however a special thing about lazy expressions. Its tag changes when evaluated. (A ref type like I have proposed has a constant 0 tag).

utop # let l = lazy (5+8);;
val l : int lazy_t = <lazy>
utop # Obj.tag @@ Obj.repr @@ l;;
- : int = 246
utop # Lazy.force l;;
- : int = 13
utop # Obj.tag @@ Obj.repr @@ l;;
- : int = 250