let sysf_cons x xs = fun c n -> fun () -> c x (xs c n);;
let sysf_length xs = xs (fun x z -> z () + 1) (fun () -> 0) ();;
-Notice that we have `sysf_cons` returning a `fun () ->`, and also that in `sysf_length` we have to apply a `()` to the seed argument to evaluate it and extract its value, and also we apply a `()` to the output of the `sysf_length` function.
+Notice that we have `sysf_cons` returning a `fun () ->`, and also that in `sysf_length` we have to apply a `()` to the seed argument to evaluate it and extract its value. That's a good thing, we don't *want* to automatically evaluate the fold over the rest of the list if doing so might invoke a `blackhole` or `failwith`. We only want the fold over the rest of the list to be evaluated when we specifically request it, by feeding the thunk a `()` argument. (This is called "forcing the thunk.") Also, after the fold has traversed the whole list, what we'll have at that point will be a thunk (it has to have the same type as the seed value). So we have to force it to get our answer --- that's why there's a `()` at the end of `sysf_length`.
Now how are we doing?
type ('a) mylist = Cons of 'a * ('a) mylist | Nil
And you won't have any of the kinds of difficulties we're discussing here with that. It's just that some of the topics we're exploring in this course press against the walls where things are hard (or sometimes not even possible) to do in OCaml (and sometimes Haskell too).
+
+By the way, this issue about not-enough-polymorphism doesn't arise in Haskell. Here are the Church numerals:
+
+ > type Church a = (a -> a) -> a -> a
+ > let { zero :: Church a; zero = \s z -> z; one :: Church a; one = \s z -> s z; succ n = \s z-> s (n s z) }
+ > let two = succ one
+ > two ('S':) "0"
+ "SS0"
+ > :t two
+ two :: (a -> a) -> a -> a
+ > two (1+) 0
+ 2
+
+The reason that OCaml has trouble here where Haskell doesn't has to do with some fundamental differences between their type systems, that we haven't yet explored. (Specifically, it has to do with the fact that OCaml has *mutable reference cells* in its type system, and this obliges it to place limits on where it generalizes type variables, else its type system becomes inconsistent.)