monads
[lambda.git] / exercises / assignment5_hint4.mdwn
1 There are two ways to approach encoding a list in System F / OCaml. One way thinks of the list in the style of OCaml's datatypes:
2
3     type ('a) mylist = Cons of 'a * ('a) mylist | Nil
4
5 Now in general it is possible to encode sum types like this in System F. The idea would be to make the list be a higher-order function that accepted two arguments. One argument would be the Cons-handler, the other the Nil-handler. If the list in question were non-empty, it would ignore the Nil-handler and instead feed its head and its tail to the Cons-handler. If the list were on the other hand empty, it would ignore the Cons handler and instead just return the Nil-handler.
6
7 That basic idea is fine, but there are obstacles to encoding it in System F and different obstacles to encoding it (in that style) in OCaml. (The above type declaration works fine in OCaml, though.)
8
9 What is the obstacle to encoding it in System F? Well think about what the type would be. Something like this:
10
11     type mylist = forall 'a. forall 'b. ('a -> __ -> 'b) -> 'b -> 'b
12
13 Wait, what goes in the blank spot. That has to be the type of mylist's tail. But that should again be the same type as mylist. And we don't know how to make types that refer to themselves, and indeed in System F itself, it is impossible to do so.
14
15 Even if you could, you wouldn't be able to *do* too much with lists encoded in this way, because in System F there's no `letrec`.
16
17 So the more promising way forward would be to use the other approach to encoding a list in System F / OCaml, which instead encodes the lists in terms of their right-folds. We will explore that further below. You may want to skip to END DIGRESSION the first time you read this (though the end of this discussion will refer back to some of the stuff explained during the digression).
18
19 START DIGRESSION
20
21 First, a lengthy digression about how we might nonetheless pursue this first encoding strategy in OCaml instead. Of course you don't *have to* encode lists in OCaml. OCaml already gives you its native lists `[10, 20, 30]`, and even if it didn't, you could just write a datatype declaration for mylist like we have above, and then use that, with `letrec` and `match` and so on just as we were doing in the early weeks of class. Only now with pretty types.
22
23 Still, it may be instructive to see how we would encode lists in the style we described. It may help us understand better what's going on behind that datatype declaration, and it will also show us some of the constraints that OCaml labors under, and that sometimes one needs to work around.
24
25 So the type we want would be something like this:
26
27     type mylist = forall 'a. forall 'b. ('a -> mylist -> 'b) -> 'b -> 'b
28
29 One problem though is that OCaml doesn't understand those `forall`s. Well, we can just parameterize the list on the `'a`, since if we have a list of `'a`s, it will always be a list of `'a`s.
30
31     type ('a) mylist = forall 'b. ('a -> ('a) mylist -> 'b) -> 'b -> 'b
32
33 We should be a bit reluctant to parameterize on the `'b`s, though, because let's say we encode a list `[10,20,30]`. That can intrinsically be a list where the `'a`s are `int`s, but it shouldn't intrinsically be a list where the `'b` result type is `char` or `bool` or `int` or anything in particular. We want one and the same list to be capable of delivering any of those results depending on what is the type of the handlers passed to it.
34
35 If we just omitted the `forall 'b.`, though, OCaml would complain that our type declaration has an unbound type variable in it:
36
37     # type ('a) mylist = ('a -> ('a) mylist -> 'b) -> 'b -> 'b;;
38     Error: Unbound type parameter 'b
39
40 So let's try parameterizing on the `'b` variable too, and seeing how it works out. If we just try to do it like this:
41
42     type ('a,'b) sysf_list = ('a -> ('a,'b) sysf_list -> 'b) -> 'b -> 'b;;
43
44 OCaml won't like that either:
45
46     # type ('a,'b) sysf_list = ('a -> ('a,'b) sysf_list -> 'b) -> 'b -> 'b;;
47     Error: The type abbreviation sysf_list is cyclic
48
49 Now OCaml can tolerate recursive types, but only if the recursive call isn't "naked": it has to be underneath a constructor or something else of that sort. So we could do this instead, adding a constructor `S` around the whole type:
50
51     type ('a,'b) sysf_list = S of (('a -> ('a,'b) sysf_list -> 'b) -> 'b -> 'b);;
52
53 OCaml will accept that. You can't have been expected to know that this would be needed. But then, we didn't intend for you to go down this path anyway. We intended for you to encode the lists in terms of their right-folds, which we discuss below. This long digression is just a learning exercise about how things work out if you stick with the first encoding style.
54
55 Now with this type definition, we can define a few list functions. The tricky part is making sure to pop off the `S`'s when we want access to the higher-order function that is the `sysf_list`'s body, and to wrap an `S` back around the result when we want to call it an official `sysf_list` again.
56
57     let sysf_empty = S (fun ht n -> n);;
58     let sysf_cons x xs = S (fun ht n -> ht x xs);;
59     let sysf_isempty (S xs) = xs (fun h t -> false) true;;
60     let sysf_head (S xs) = xs (fun h t -> h) __;;
61
62 Well, what should we use as the second value if `sysf_head` is applied to a `sysf_empty` list? If we knew that it was an `(int, _) sysf_list`, we could perhaps return `0`, if a `(char, _) sysf_list`, we could perhaps return a space character, or make some other arbitrary choice. But it's clear we don't have any general, principled solution here.
63
64 But at this point, perhaps you can apply some of the things you learned from other parts of the assignment. Look at the type of the `blackhole` function:
65
66     # let rec blackhole () = blackhole ();;
67     val blackhole : unit -> 'a = <fun>
68
69 It's a function from `unit -> 'a`, for *any `'a` whatsoever*! All of OCaml's functions that don't return to their callers, but which go into infinite loops, and also the functions that raise an error, have this property. Here's another one, one of OCaml's built-in error functions:
70
71     # failwith;;
72     - : string -> 'a = <fun>
73
74 So perhaps we could define `sysf_head` like this:
75
76     let sysf_head (S xs) = xs (fun h t -> h) (failwith "bad list");;
77
78 And indeed that will type perfectly. Unfortunately, though, guess what happens if we apply that function to a good list:
79
80     # let abc = sysf_cons 'a' (sysf_cons 'b' (sysf_cons 'c' sysf_empty));;
81     # sysf_head abc;;
82     Exception: Failure "bad list".
83
84 Why? Because OCaml, like most programming languages, is call-by-value. So the argument `failwith "bad list"` gets evaluated *before* its result is passed into the xs function, and thus the `xs` function never gets invoked.
85
86 How can we avoid this? If only we had a way of scheduling that failure, but suspending its evaluation so that it didn't happen right when we scheduled it, but only (perhaps) later, if the `xs` function corresponds to an empty list and so tries to use it. Have you seen any way of doing that?
87
88 Yes you have. The idea is to write `sysf_head` like this instead:
89
90     let sysf_head (S xs) = xs (fun h t -> h) (fun () -> failwith "bad list");;
91
92 Of course, that won't type right. (OCaml will accept that definition ok, but the types will be screwed up later when you try to combine it with lists built using the `sysf_cons` we've got.) The problem is that now we are thinking that the second, if-you're-empty argument is always a thunk, so we should rewrite all our definitions with this in mind.
93
94     type ('a,'b) sysf_list = S of (('a -> ('a,'b) sysf_list -> 'b) -> (unit -> 'b) -> 'b);;
95                                                                        -------
96     let sysf_empty = S (fun ht n -> n ());;
97                                       --
98     let sysf_cons x xs = S (fun ht n -> ht x xs);;
99     let sysf_isempty (S xs) = xs (fun h t -> false) (fun () -> true);;
100                                                      ---------
101     let sysf_head (S xs) = xs (fun h t -> h) (fun () -> failwith "bad list");;
102                                               ---------
103
104 All the changes have been underlined. Now, this is looking a lot better. In fact, it almost works.
105
106     # let abc = sysf_cons 'a' (sysf_cons 'b' (sysf_cons 'c' sysf_empty));;
107     val abc : (char, '_b) sysf_list = S <fun>
108
109 Looks good, what's the problem? The hint that there's trouble comes in the type OCaml displays for the list `abc` you just created. Its type is `(char, '_b) sysf_list`. Notice that `'_b` type parameter begins with an underscore. That's OCaml's convention for indicating that it is not polymorphic or generalized over. It's some specific one type; OCaml just hasn't figured out what that type is yet. But as that `abc` list interacts with other pieces of code, OCaml will eventually decide that it has one specific type, and then it will insist that that must always be the second type parameter, and thus must always be the type of the result returned by the handlers.
110
111 For example:
112
113     # let S xs = abc in xs (fun h t -> 1) (fun () -> 0);;
114     - : int = 1
115     # abc;;
116     - : (char, int) sysf_list = S <fun>
117
118 Now it has decided `abc` only takes handlers returning int results:
119
120     # let S xs = abc in xs (fun h t -> true) (fun () -> false);;
121                                        ----
122     Error: This expression has type bool but an expression was expected of type int
123
124 Whoops. This is exactly the problem I warned we were going to encounter by making the result type a parameter for the list type, on a par with `'a`. Any given list is a list of a *specific type* of `'as`; but it shouldn't be a list that only returns type a specific type `'b` result. It should be able to return any type result, depending on what handlers are passed to it.
125
126 There is a way to do this in OCaml, but it has to use some apparatus you haven't been introduced to yet. The lightest-weight way to do it would be to use OCaml's "polymorphic record types". Here is how it looks, if you're curious. The `{ label = ...}` is OCaml's syntax for a "record", something like a tuple but with the field referred to by its label rather than by its position. The `'b.` at the start of the type declaration for the record's field is OCaml's way of saying `forall b.`:
127
128     # type ('a) sysf_list = { sysf_list : 'b. ('a -> ('a) sysf_list -> 'b) -> (unit -> 'b) -> 'b };;
129     # let sysf_empty = { sysf_list = fun ht n -> n () };;
130     # let sysf_cons (x:'a) (xs:('a) sysf_list) : ('a) sysf_list = { sysf_list = fun ht n -> ht x xs };;
131     # let sysf_isempty xs = xs.sysf_list (fun h t -> false) (fun () -> true);;
132     # let sysf_head xs = xs.sysf_list (fun h t -> h) (fun () -> failwith "never");;
133     # let sysf_tail xs = xs.sysf_list (fun h t -> t) (fun () -> sysf_empty);;
134
135     # let abc = sysf_cons 'a' (sysf_cons 'b' (sysf_cons 'c' sysf_empty));;
136     # let { sysf_list = xs } = abc in xs (fun h t -> 1) (fun () -> 0);;
137     - : int = 1
138     # let { sysf_list = xs } = abc in xs (fun h t -> true) (fun () -> false);;
139     - : bool = true
140
141 No problem. Again, there was no way you could be expected to know that these contortions would be necessary.
142
143 END DIGRESSION
144
145 Okay, so if the approach of encoding lists the way we encode sum-types isn't going to fly at all in System F, or easily in OCaml, what are our alternatives. We just encode the structure using its natural recursion, like we did when we encoded lists in terms of their right-folds back in the untyped Lambda Calculus.
146
147 In System F, the idea would be this:
148
149     type sysf_list_a = forall 'b. ('a->'b->'b) -> 'b -> 'b
150
151 That is, a `sysf_list_a` encodes a list of `'a`s (we don't try to generalize on the list element, this is not possible to do in a satisfying way in System F). For every possible result type `'b`, it accepts a fold function `c:'a->'b->'b` and a seed value `n:'b` keyed to that result type, and returns a result of that type (what you get by right-folding function `c` over the list using that seed value `n`).
152
153     let sysf_empty_a = Lambda 'b. \c:'a->'b->'b. \n:'b. n
154     let sysf_cons_a = \x:'a. \xs:sysf_list_a. Lambda 'b. \c:'a->'b->'b. \n:'b. c x (xs ['b] c n)
155     let sysf_isempty_a = \xs:sysf_list_a. xs [Boolean] (\_:'a. \_:Boolean. false) true
156     let sysf_head_a = \xs:sysf_list_a. xs ['a] (\x:'a. \_:'a. x) (some_arbitrarily_chosen_value_of_type_a)
157
158 And if only we had asked you to stop there, all would be good.
159
160 Unfortunately, though, we encouraged you to try to get this to work in OCaml. Here is a first attempt. In OCaml we can even parameterize on the type of the list element, so we can write `('a) sysf_list` instead of `sysf_list_a`. Also, in OCaml we omit the `Lambda 'b`s and the `[Type]`s. Also the syntax for lambda expressions is a bit different. But those are the only changes I'm making here from the System F code:
161
162     type ('a) sysf_list = ('a->'b->'b) -> 'b -> 'b
163
164     let sysf_empty : ('a) sysf_list = fun (c:'a->'b->'b) (n:'b) -> n
165     let sysf_cons (x:'a) (xs:('a) sysf_list) = fun (c:'a->'b->'b) (n:'b) -> c x (xs c n)
166     let sysf_isempty (xs:('a) sysf_list) = xs (fun (_:'a) (_:bool) -> false) true
167     let sysf_head (xs:('a) sysf_list) = xs (fun (x:'a) (_:'a) -> x) (some_arbitrarily_chosen_value_of_type_a)
168
169 Whoops. Isn't this just going to inherit most of the same problems discussed above in the digression? We can fix the issue of `some_arbitrarily_chosen_value_of_type_a` by using `fun () -> failwith "bad list"` or `fun () -> blackhole ()`. It's a bit trickier here, because the type of the seed value `n` has to be *the same type* as is returned when the fold function `c` is applied to its two arguments (the current element and the result of folding over the rest of the list). So we have to add `fun () ->` to everything returned by the fold functions, too. And then at the end of our functions, we should discharge the `fun () ->` by supplying a `()` argument. But all of that is doable.
170
171 Still, the problem of that unbound type parameter `'b`, that we want to be generalized/polymorphic, remains.
172
173 If we just decline to specify the types, OCaml will infer them for us:
174
175     let sysf_empty = fun c (n : unit -> 'b) -> n;;
176     let sysf_cons x xs = fun c n -> fun () -> c x (xs c n);;
177     let sysf_length xs = xs (fun x z -> z () + 1) (fun () -> 0) ();;
178
179 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`.
180
181 Now how are we doing?
182
183     # let abc = sysf_cons 'a' (sysf_cons 'b' (sysf_cons 'c' sysf_empty));;
184     val abc : (char -> (unit -> '_b) -> '_b) -> (unit -> '_b) -> unit -> '_b =  <fun>
185
186 Uh-oh. There are those `'_b` types again. It means OCaml has decided this list can only have a single result type, it just doesn't know what it is yet. But once you pass one handler to the list, it will be settled and can't afterwards be changed.
187
188     # abc (fun x _ -> 1) (fun () -> 0) ();;
189     - : int = 1
190     # abc;;
191     - : (char -> (unit -> int) -> int) -> (unit -> int) -> unit -> int = <fun>
192     # abc (fun x _ -> true) (fun () -> false) ();;
193                       ----
194     Error: This expression has type bool but an expression was expected of type int
195
196 The lightest-weight way to fix this issue would again be to use OCaml's "polymorphic record types", discussed above in the digression, and which you can't be expected to know about. So really we should have done this assignment differently, perhaps just in System F. Well, sorry. You will hopefully have learned something from the experience of trying to get it to work, and in the end working through this explanation of why it was harder than it seemed it should be. We hope that the frustration and confusion didn't undermine that learning benefit too much. We in turn learned something too, that this problem wasn't as straightforward as we expected it to be.
197
198
199 For reference, here is how I'd encode lists as right-folds, using OCaml's polymorphic record types:
200
201     type ('a) sysf_list = { sysf_list2 : 'b. ('a->(unit->'b)->'b) -> (unit -> 'b) -> unit -> 'b };;
202
203     let sysf_empty : ('a) sysf_list = { sysf_list2 = fun c n -> n };;
204     let sysf_cons (x:'a) (xs:('a) sysf_list) : ('a) sysf_list = { sysf_list2 = fun c n () -> c x (xs.sysf_list2 c n) };;
205
206 If you try to specify type annotations on the `c` and `n` arguments in `sysf_empty` and `sysf_cons`, like this:
207
208     let sysf_empty : ('a) sysf_list = { sysf_list2 = fun (c:'a->(unit->'b)->'b) (n:unit->'b) -> n };;
209     let sysf_cons (x:'a) (xs:('a) sysf_list) : ('a) sysf_list = { sysf_list2 = fun (c:'a->(unit->'b)->'b) (n:unit->'b) () -> c x (xs.sysf_list2 c n) };;
210
211 OCaml will complain that the types aren't general enough. I don't know how to fix this, other than to omit those type annotations, as I did above.
212
213 Here are some more list functions:
214
215     let sysf_length (xs:('a) sysf_list) : int = xs.sysf_list2 (fun x z -> z () + 1) (fun () -> 0) ();;
216     let sysf_isempty (xs:('a) sysf_list) = xs.sysf_list2 (fun (y:'a) (_:unit->bool) -> false) (fun () -> true) ();;
217     let sysf_head (xs:('a) sysf_list) = xs.sysf_list2 (fun (y:'a) (_:unit->'a) -> y) (fun () -> failwith "bad list") ();;
218
219     # let abc = sysf_cons 'a' (sysf_cons 'b' (sysf_cons 'c' sysf_empty));;
220     val abc : char sysf_list = {sysf_list2 = <fun>}
221     # sysf_isempty abc;;
222     - : bool = false
223     # sysf_isempty sysf_empty;;
224     - : bool = true
225     # sysf_length sysf_empty;;
226     - : int = 0
227     # sysf_length abc;;
228     - : int = 3
229     # sysf_head abc;;
230     - : char = 'a'
231     # sysf_head sysf_empty;;
232     Exception: Failure "bad list".
233
234 Yes, they do work as expected.
235
236
237 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:
238
239     # type 'b sysf_nat = ('b -> 'b) -> 'b -> 'b
240     let sysf_zero : ('b) sysf_nat = fun s z -> z
241     let sysf_one : ('b) sysf_nat = fun s z -> s z
242     let sysf_succ : ('b) sysf_nat -> ('b) sysf_nat = fun n -> (fun s z -> s (n s z));;
243
244     # sysf_succ sysf_one;;
245     - : '_b sysf_nat = <fun>
246
247 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.
248
249 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:
250
251     # fun s -> sysf_succ sysf_one s;;
252     - : ('a -> 'a) -> 'a -> 'a = <fun>
253
254 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.
255
256 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.
257
258     type ('a) mylist = Cons of 'a * ('a) mylist | Nil
259
260 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).
261
262 By the way, this issue about not-enough-polymorphism doesn't arise in Haskell. Here are the Church numerals:
263
264     > type Church a = (a -> a) -> a -> a
265     > let { zero :: Church a; zero = \s z -> z; one :: Church a; one = \s z -> s z; succ n = \s z-> s (n s z) }
266     > let two = succ one
267     > two ('S':) "0"
268     "SS0"
269     > :t two
270     two :: (a -> a) -> a -> a
271     > two (1+) 0
272     2
273
274 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.)