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?
Yes, they do work as expected.
+
+By the way, the main problem here (of OCaml not making the functions polymorphic enough) will also afflict your attempts to encode Church numerals, though you might not have noticed it there. But witness:
+
+ # type 'b sysf_nat = ('b -> 'b) -> 'b -> 'b
+ let sysf_zero : ('b) sysf_nat = fun s z -> z
+ let sysf_one : ('b) sysf_nat = fun s z -> s z
+ let sysf_succ : ('b) sysf_nat -> ('b) sysf_nat = fun n -> (fun s z -> s (n s z));;
+
+ # sysf_succ sysf_one;;
+ - : '_b sysf_nat = <fun>
+
+Notice the `'_b` type parameter. That means that OCaml thinks the successor of `sysf_one` is not polymorphic, but always will be giving only a single result type. OCaml just doesn't yet know what it is.
+
+There is one easy-to-implement fix to this problem. If instead of `sysf_succ sysf_one` you had instead written the eta-expanded version:
+
+ # fun s -> sysf_succ sysf_one s;;
+ - : ('a -> 'a) -> 'a -> 'a = <fun>
+
+then OCaml knows to make the result polymorphic. But it's a pain to force yourself to write `fun s -> ... s` around all of your arithmetical computations. Short of doing that, the only way I know to make OCaml treat these functions as polymorphic enough is to use the "polymorphic record types" discussed above.
+
+This kind of problem doesn't come up *that* often in OCaml. Normally, you wouldn't be encoding your data structures in this way, anyway. You'd use some datatype declaration like we had at the top of this page.
+
+ 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.)