From: jim
Date: Sun, 8 Mar 2015 02:47:32 +0000 (-0500)
Subject: add more about numbers
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=2b1a1038f33af64c6d2f5f40ca3ff65ccc667b86
add more about numbers
---
diff --git a/exercises/assignment5_hint4.mdwn b/exercises/assignment5_hint4.mdwn
index 447852e9..7ef02c6a 100644
--- a/exercises/assignment5_hint4.mdwn
+++ b/exercises/assignment5_hint4.mdwn
@@ -233,3 +233,28 @@ Here are some more list functions:
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 =
+
+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 =
+
+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).