+
+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).