X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2Fassignment5_hint4.mdwn;h=d718c9a7c01c5af843c731b43ff08616bc1c6cc2;hp=7ef02c6ab263a31573c1b20cbc7d79bb3735ef25;hb=7888d341776f23849c60cd82ca816ed13e5bc9c2;hpb=2b1a1038f33af64c6d2f5f40ca3ff65ccc667b86

diff --git a/exercises/assignment5_hint4.mdwn b/exercises/assignment5_hint4.mdwn
index 7ef02c6a..d718c9a7 100644
--- a/exercises/assignment5_hint4.mdwn
+++ b/exercises/assignment5_hint4.mdwn
@@ -176,7 +176,7 @@ If we just decline to specify the types, OCaml will infer them for us:
     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?
 
@@ -258,3 +258,17 @@ This kind of problem doesn't come up *that* often in OCaml. Normally, you wouldn
     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.)