X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2Fassignment5_hint4.mdwn;h=8c65df17d6124896a6d96ed9b3b6b1b8556041b1;hp=498d7b3b549e93b9d96f2927f8d3d5715689488c;hb=67cb14b0d6067d3024d34c8e72febd07b8f33b3f;hpb=7c7072d47d231e4d4f86b229fb3877d1c3f921e2

diff --git a/exercises/assignment5_hint4.mdwn b/exercises/assignment5_hint4.mdwn
index 498d7b3b..8c65df17 100644
--- a/exercises/assignment5_hint4.mdwn
+++ b/exercises/assignment5_hint4.mdwn
@@ -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 unsound.)