(no commit message)
[lambda.git] / topics / _week5_system_F.mdwn
1 [[!toc levels=2]]
2
3 # System F and recursive types
4
5 In the simply-typed lambda calculus, we write types like <code>&sigma;
6 -> &tau;</code>.  This looks like logical implication.  We'll take
7 that resemblance seriously when we discuss the Curry-Howard
8 correspondence.  In the meantime, note that types respect modus
9 ponens: 
10
11 <pre>
12 Expression    Type      Implication
13 -----------------------------------
14 fn            &alpha; -> &beta;    &alpha; &sup; &beta;
15 arg           &alpha;         &alpha;
16 ------        ------    --------
17 (fn arg)      &beta;         &beta;
18 </pre>
19
20 The implication in the right-hand column is modus ponens, of course.
21
22 System F was discovered by Girard (the same guy who invented Linear
23 Logic), but it was independently proposed around the same time by
24 Reynolds, who called his version the *polymorphic lambda calculus*.
25 (Reynolds was also an early player in the development of
26 continuations.)  
27
28 System F enhances the simply-typed lambda calculus with abstraction
29 over types.  Normal lambda abstraction abstracts (binds) an expression
30 (a term); type abstraction abstracts (binds) a type.
31
32 In order to state System F, we'll need to adopt the
33 notational convention (which will last throughout the rest of the
34 course) that "<code>x:&alpha;</code>" represents an expression `x`
35 whose type is <code>&alpha;</code>.
36
37 Then System F can be specified as follows (choosing notation that will
38 match up with usage in O'Caml, whose type system is based on System F):
39
40         System F:
41         ---------
42         types τ ::= c | α | τ1 -> τ2 | ∀'a. τ
43         expressions e ::= x | λx:τ. e | e1 e2 | Λα. e | e [τ]
44
45 In the definition of the types, "`c`" is a type constant.  Type
46 constants play the role in System F that base types play in the
47 simply-typed lambda calculus.  So in a lingusitics context, type
48 constants might include `e` and `t`.  "α" is a type variable.  The
49 tick mark just indicates that the variable ranges over types rather
50 than over values; in various discussion below and later, type variable
51 can be distinguished by using letters from the greek alphabet
52 (&alpha;, &beta;, etc.), or by using capital roman letters (X, Y,
53 etc.).  "`τ1 -> τ2`" is the type of a function from expressions of
54 type `τ1` to expressions of type `τ2`.  And "`∀α. τ`" is called a
55 universal type, since it universally quantifies over the type variable
56 `'a`.  You can expect that in `∀α. τ`, the type `τ` will usually
57 have at least one free occurrence of `α` somewhere inside of it.
58
59 In the definition of the expressions, we have variables "`x`" as usual.
60 Abstracts "`λx:τ. e`" are similar to abstracts in the simply-typed lambda
61 calculus, except that they have their shrug variable annotated with a
62 type.  Applications "`e1 e2`" are just like in the simply-typed lambda calculus.
63
64 In addition to variables, abstracts, and applications, we have two
65 additional ways of forming expressions: "`Λα. e`" is called a *type
66 abstraction*, and "`e [τ]`" is called a *type application*.  The idea
67 is that <code>&Lambda;</code> is a capital <code>&lambda;</code>: just
68 like the lower-case <code>&lambda;</code>, <code>&Lambda;</code> binds
69 variables in its body, except that unlike <code>&lambda;</code>,
70 <code>&Lambda;</code> binds type variables instead of expression
71 variables.  So in the expression
72
73 <code>&Lambda; α (&lambda; x:α . x)</code>
74
75 the <code>&Lambda;</code> binds the type variable `α` that occurs in
76 the <code>&lambda;</code> abstract.  Of course, as long as type
77 variables are carefully distinguished from expression variables (by
78 tick marks, Grecification, or capitalization), there is no need to
79 distinguish expression abstraction from type abstraction by also
80 changing the shape of the lambda.
81
82 The expression immediately below is a polymorphic version of the
83 identity function.  It defines one general identity function that can
84 be adapted for use with expressions of any type. In order to get it
85 ready to apply this identity function to, say, a variable of type
86 boolean, just do this:
87
88 <code>(&Lambda; α (&lambda; x:α . x)) [t]</code>    
89
90 This type application (where `t` is a type constant for Boolean truth
91 values) specifies the value of the type variable `α`.  Not
92 surprisingly, the type of this type application is a function from
93 Booleans to Booleans:
94
95 <code>((&Lambda; α (&lambda; x:α . x)) [t]): (b -> b)</code>    
96
97 Likewise, if we had instantiated the type variable as an entity (base
98 type `e`), the resulting identity function would have been a function
99 of type `e -> e`:
100
101 <code>((&Lambda; α (&lambda; x:α . x)) [e]): (e -> e)</code>    
102
103 Clearly, for any choice of a type `α`, the identity function can be
104 instantiated as a function from expresions of type `α` to expressions
105 of type `α`.  In general, then, the type of the uninstantiated
106 (polymorphic) identity function is
107
108 <code>(&Lambda; α (&lambda; x:α . x)): (&forall; α . α -> α)</code>
109
110 Pred in System F
111 ----------------
112
113 We saw that the predecessor function couldn't be expressed in the
114 simply-typed lambda calculus.  It *can* be expressed in System F,
115 however.  Here is one way, coded in
116 [[Benjamin Pierce's type-checker and evaluator for
117 System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
118 relevant evaluator is called "fullpoly"):
119
120     N = ∀ α . (α->α)->α->α;
121     Pair = (N -> N -> N) -> N;
122     let zero = lambda α . lambda s:α->α . lambda z:α. z in 
123     let fst = lambda x:N . lambda y:N . x in
124     let snd = lambda x:N . lambda y:N . y in
125     let pair = lambda x:N . lambda y:N . lambda z:N->N->N . z x y in
126     let suc = lambda n:N . lambda α . lambda s:α->α . lambda z:α . s (n [α] s z) in
127     let shift = lambda p:Pair . pair (suc (p fst)) (p fst) in
128     let pre = lambda n:N . n [Pair] shift (pair zero zero) snd in
129
130     pre (suc (suc (suc zero)));
131
132 We've truncated the names of "suc(c)" and "pre(d)", since those are
133 reserved words in Pierce's system.  Note that in this code, there is
134 no typographic distinction between ordinary lambda and type-level
135 lambda, though the difference is encoded in whether the variables are
136 lower case (for ordinary lambda) or upper case (for type-level
137 lambda).
138
139 The key to the extra expressive power provided by System F is evident
140 in the typing imposed by the definition of `pre`.  The variable `n` is
141 typed as a Church number, i.e., as `∀ α . (α->α)->α->α`.  The type
142 application `n [Pair]` instantiates `n` in a way that allows it to
143 manipulate ordered pairs: `n [Pair]: (Pair->Pair)->Pair->Pair`.  In
144 other words, the instantiation turns a Church number into a
145 pair-manipulating function, which is the heart of the strategy for
146 this version of predecessor.  
147
148 Could we try to build a system for doing Church arithmetic in which
149 the type for numbers always manipulated ordered pairs?  The problem is
150 that the ordered pairs we need here are pairs of numbers.  If we tried
151 to replace the type for Church numbers with a concrete (simple) type,
152 we would have to replace each `X` with the type for Pairs, `(N -> N ->
153 N) -> N`.  But then we'd have to replace each of these `N`'s with the
154 type for Church numbers, `(α -> α) -> α -> α`.  And then we'd have to
155 replace each of these `α`'s with... ad infinitum.  If we had to choose
156 a concrete type built entirely from explicit base types, we'd be
157 unable to proceed.
158  
159 [See Benjamin C. Pierce. 2002. *Types and Programming Languages*, MIT
160 Press, chapter 23.]
161
162 Typing &omega;
163 --------------
164
165 In fact, unlike in the simply-typed lambda calculus, 
166 it is even possible to give a type for &omega; in System F. 
167
168 <code>&omega; = lambda x:(∀ α. α->α) . x [∀ α . α->α] x</code>
169
170 In order to see how this works, we'll apply &omega; to the identity
171 function.  
172
173 <code>&omega; id ==</code>
174
175     (lambda x:(∀ α . α->α) . x [∀ α . α->α] x) (lambda α . lambda x:α . x)
176
177 Since the type of the identity function is `(∀ α . α->α)`, it's the
178 right type to serve as the argument to &omega;.  The definition of
179 &omega; instantiates the identity function by binding the type
180 variable `α` to the universal type `∀ α . α->α`.  Instantiating the
181 identity function in this way results in an identity function whose
182 type is (in some sense, only accidentally) the same as the original
183 fully polymorphic identity function.
184
185 So in System F, unlike in the simply-typed lambda calculus, it *is*
186 possible for a function to apply to itself!
187
188 Does this mean that we can implement recursion in System F?  Not at
189 all.  In fact, despite its differences with the simply-typed lambda
190 calculus, one important property that System F shares with the
191 simply-typed lambda calculus is that they are both strongly
192 normalizing: *every* expression in either system reduces to a normal
193 form in a finite number of steps.  
194
195 Not only does a fixed-point combinator remain out of reach, we can't
196 even construct an infinite loop.  This means that although we found a
197 type for &omega;, there is no general type for &Omega; &equiv; &omega;
198 &omega;.  Furthermore, it turns out that no Turing complete system can
199 be strongly normalizing, from which it follows that System F is not
200 Turing complete.
201
202
203 ## Polymorphism in natural language
204
205 Is the simply-typed lambda calclus enough for analyzing natural
206 language, or do we need polymorphic types? Or something even more expressive?
207
208 The classic case study motivating polymorphism in natural language
209 comes from coordination.  (The locus classicus is Partee and Rooth
210 1983.)
211
212     Ann left and Bill left.
213     Ann left and slept.
214     Ann and Bill left.
215     Ann read and reviewed the book.
216
217 In English (likewise, many other languages), *and* can coordinate
218 clauses, verb phrases, determiner phrases, transitive verbs, and many
219 other phrase types.  In a garden-variety simply-typed grammar, each
220 kind of conjunct has a different semantic type, and so we would need
221 an independent rule for each one.  Yet there is a strong intuition
222 that the contribution of *and* remains constant across all of these
223 uses.  Can we capture this using polymorphic types?
224
225     Ann, Bill      e
226     left, slept    e -> t    
227     read, reviewed e -> e -> t
228
229 With these basic types, we want to say something like this:
230
231     and:t->t->t = lambda l:t . lambda r:t . l r false
232     and = lambda α . lambda β . 
233             lambda l:α->β . lambda r:α->β . 
234               lambda x:α . and:β (l x) (r x)
235
236 The idea is that the basic *and* conjoins expressions of type `t`, and
237 when *and* conjoins functional types, it builds a function that
238 distributes its argument across the two conjuncts and conjoins the two
239 results.  So `Ann left and slept` will evaluate to `(\x.and(left
240 x)(slept x)) ann`.  Following the terminology of Partee and Rooth, the
241 strategy of defining the coordination of expressions with complex
242 types in terms of the coordination of expressions with less complex
243 types is known as Generalized Coordination.
244
245 But the definitions just given are not well-formed expressions in
246 System F.  There are three problems.  The first is that we have two
247 definitions of the same word.  The intention is for one of the
248 definitions to be operative when the type of its arguments is type
249 `t`, but we have no way of conditioning evaluation on the *type* of an
250 argument.  The second is that for the polymorphic definition, the term
251 *and* occurs inside of the definition.  System F does not have
252 recursion.  
253
254 The third problem is more subtle.  The defintion as given takes two
255 types as parameters: the type of the first argument expected by each
256 conjunct, and the type of the result of applying each conjunct to an
257 argument of that type.  We would like to instantiate the recursive use
258 of *and* in the definition by using the result type.  But fully
259 instantiating the definition as given requires type application to a
260 pair of types, not to just a single type.  We want to somehow
261 guarantee that β will always itself be a complex type.
262
263 So conjunction and disjunction provide a compelling motivation for
264 polymorphism in natural language, but we don't yet have the ability to
265 build the polymorphism into a formal system.
266
267 And in fact, discussions of generalized coordination in the
268 linguistics literature are almost always left as a meta-level
269 generalizations over a basic simply-typed grammar.  For instance, in
270 Hendriks' 1992:74 dissertation, generalized coordination is
271 implemented as a method for generating a suitable set of translation
272 rules, which are in turn expressed in a simply-typed grammar.
273
274 Not incidentally, we're not aware of any programming language that
275 makes generalized coordination available, despite is naturalness and
276 ubiquity in natural language.  That is, coordination in programming
277 languages is always at the sentential level.  You might be able to
278 evaluate `(delete file1) and (delete file2)`, but never `delete (file1
279 and file2)`.
280
281 We'll return to thinking about generalized coordination as we get
282 deeper into types.  There will be an analysis in term of continuations
283 that will be particularly satisfying.
284
285
286 #Types in OCaml
287
288
289 OCaml has type inference: the system can often infer what the type of
290 an expression must be, based on the type of other known expressions.
291
292 For instance, if we type
293
294     # let f x = x + 3;;
295
296 The system replies with
297
298     val f : int -> int = <fun>
299
300 Since `+` is only defined on integers, it has type
301
302      # (+);;
303      - : int -> int -> int = <fun>
304
305 The parentheses are there to turn off the trick that allows the two
306 arguments of `+` to surround it in infix (for linguists, SOV) argument
307 order. That is,
308
309     # 3 + 4 = (+) 3 4;;
310     - : bool = true
311
312 In general, tuples with one element are identical to their one
313 element:
314
315     # (3) = 3;;
316     - : bool = true
317
318 though OCaml, like many systems, refuses to try to prove whether two
319 functional objects may be identical:
320
321     # (f) = f;;
322     Exception: Invalid_argument "equal: functional value".
323
324 Oh well.
325
326 [Note: There is a limited way you can compare functions, using the
327 `==` operator instead of the `=` operator. Later when we discuss mutation,
328 we'll discuss the difference between these two equality operations.
329 Scheme has a similar pair, which they name `eq?` and `equal?`. In Python,
330 these are `is` and `==` respectively. It's unfortunate that OCaml uses `==` for the opposite operation that Python and many other languages use it for. In any case, OCaml will accept `(f) == f` even though it doesn't accept
331 `(f) = f`. However, don't expect it to figure out in general when two functions
332 are equivalent. (That question is not Turing computable.)
333
334         # (f) == (fun x -> x + 3);;
335         - : bool = false
336
337 Here OCaml says (correctly) that the two functions don't stand in the `==` relation, which basically means they're not represented in the same chunk of memory. However as the programmer can see, the functions are extensionally equivalent. The meaning of `==` is rather weird.]
338
339
340
341 Booleans in OCaml, and simple pattern matching
342 ----------------------------------------------
343
344 Where we would write `true 1 2` in our pure lambda calculus and expect
345 it to evaluate to `1`, in OCaml boolean types are not functions
346 (equivalently, they're functions that take zero arguments). Instead, selection is
347 accomplished as follows:
348
349     # if true then 1 else 2;;
350     - : int = 1
351
352 The types of the `then` clause and of the `else` clause must be the
353 same.
354
355 The `if` construction can be re-expressed by means of the following
356 pattern-matching expression:
357
358     match <bool expression> with true -> <expression1> | false -> <expression2>
359
360 That is,
361
362     # match true with true -> 1 | false -> 2;;
363     - : int = 1
364
365 Compare with
366
367     # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
368     - : int = 9
369
370 Unit and thunks
371 ---------------
372
373 All functions in OCaml take exactly one argument.  Even this one:
374
375     # let f x y = x + y;;
376     # f 2 3;;
377     - : int = 5
378
379 Here's how to tell that `f` has been curry'd:
380
381     # f 2;;
382     - : int -> int = <fun>
383
384 After we've given our `f` one argument, it returns a function that is
385 still waiting for another argument.
386
387 There is a special type in OCaml called `unit`.  There is exactly one
388 object in this type, written `()`.  So
389
390     # ();;
391     - : unit = ()
392
393 Just as you can define functions that take constants for arguments
394
395     # let f 2 = 3;;
396     # f 2;;
397     - : int = 3;;
398
399 you can also define functions that take the unit as its argument, thus
400
401     # let f () = 3;;
402     val f : unit -> int = <fun>
403
404 Then the only argument you can possibly apply `f` to that is of the
405 correct type is the unit:
406
407     # f ();;
408     - : int = 3
409
410 Now why would that be useful?
411
412 Let's have some fun: think of `rec` as our `Y` combinator.  Then
413
414     # let rec f n = if (0 = n) then 1 else (n * (f (n - 1)));;
415     val f : int -> int = <fun>
416     # f 5;;
417     - : int = 120
418
419 We can't define a function that is exactly analogous to our &omega;.
420 We could try `let rec omega x = x x;;` what happens?
421
422 [Note: if you want to learn more OCaml, you might come back here someday and try:
423
424         # let id x = x;;
425         val id : 'a -> 'a = <fun>
426         # let unwrap (`Wrap a) = a;;
427         val unwrap : [< `Wrap of 'a ] -> 'a = <fun>
428         # let omega ((`Wrap x) as y) = x y;;
429         val omega : [< `Wrap of [> `Wrap of 'a ] -> 'b as 'a ] -> 'b = <fun>
430         # unwrap (omega (`Wrap id)) == id;;
431         - : bool = true
432         # unwrap (omega (`Wrap omega));;
433     <Infinite loop, need to control-c to interrupt>
434
435 But we won't try to explain this now.]
436
437
438 Even if we can't (easily) express omega in OCaml, we can do this:
439
440     # let rec blackhole x = blackhole x;;
441
442 By the way, what's the type of this function?
443
444 If you then apply this `blackhole` function to an argument,
445
446     # blackhole 3;;
447
448 the interpreter goes into an infinite loop, and you have to type control-c
449 to break the loop.
450
451 Oh, one more thing: lambda expressions look like this:
452
453     # (fun x -> x);;
454     - : 'a -> 'a = <fun>
455     # (fun x -> x) true;;
456     - : bool = true
457
458 (But `(fun x -> x x)` still won't work.)
459
460 You may also see this:
461
462         # (function x -> x);;
463         - : 'a -> 'a = <fun>
464
465 This works the same as `fun` in simple cases like this, and slightly differently in more complex cases. If you learn more OCaml, you'll read about the difference between them.
466
467 We can try our usual tricks:
468
469     # (fun x -> true) blackhole;;
470     - : bool = true
471
472 OCaml declined to try to fully reduce the argument before applying the
473 lambda function. Question: Why is that? Didn't we say that OCaml is a call-by-value/eager language?
474
475 Remember that `blackhole` is a function too, so we can
476 reverse the order of the arguments:
477
478     # blackhole (fun x -> true);;
479
480 Infinite loop.
481
482 Now consider the following variations in behavior:
483
484     # let test = blackhole blackhole;;
485     <Infinite loop, need to control-c to interrupt>
486
487     # let test () = blackhole blackhole;;
488     val test : unit -> 'a = <fun>
489
490     # test;;
491     - : unit -> 'a = <fun>
492
493     # test ();;
494     <Infinite loop, need to control-c to interrupt>
495
496 We can use functions that take arguments of type `unit` to control
497 execution.  In Scheme parlance, functions on the `unit` type are called
498 *thunks* (which I've always assumed was a blend of "think" and "chunk").
499
500 Question: why do thunks work? We know that `blackhole ()` doesn't terminate, so why do expressions like:
501
502         let f = fun () -> blackhole ()
503         in true
504
505 terminate?
506
507 Bottom type, divergence
508 -----------------------
509
510 Expressions that don't terminate all belong to the **bottom type**. This is a subtype of every other type. That is, anything of bottom type belongs to every other type as well. More advanced type systems have more examples of subtyping: for example, they might make `int` a subtype of `real`. But the core type system of OCaml doesn't have any general subtyping relations. (Neither does System F.) Just this one: that expressions of the bottom type also belong to every other type. It's as if every type definition in OCaml, even the built in ones, had an implicit extra clause:
511
512         type 'a option = None | Some of 'a;;
513         type 'a option = None | Some of 'a | bottom;;
514
515 Here are some exercises that may help better understand this. Figure out what is the type of each of the following:
516
517         fun x y -> y;;
518
519         fun x (y:int) -> y;;
520
521         fun x y : int -> y;;
522
523         let rec blackhole x = blackhole x in blackhole;;
524
525         let rec blackhole x = blackhole x in blackhole 1;;
526
527         let rec blackhole x = blackhole x in fun (y:int) -> blackhole y y y;;
528
529         let rec blackhole x = blackhole x in (blackhole 1) + 2;;
530
531         let rec blackhole x = blackhole x in (blackhole 1) || false;;
532
533         let rec blackhole x = blackhole x in 2 :: (blackhole 1);;
534
535 By the way, what's the type of this:
536
537         let rec blackhole (x:'a) : 'a = blackhole x in blackhole
538
539
540 Back to thunks: the reason you'd want to control evaluation with
541 thunks is to manipulate when "effects" happen. In a strongly
542 normalizing system, like the simply-typed lambda calculus or System F,
543 there are no "effects." In Scheme and OCaml, on the other hand, we can
544 write programs that have effects. One sort of effect is printing.
545 Another sort of effect is mutation, which we'll be looking at soon.
546 Continuations are yet another sort of effect. None of these are yet on
547 the table though. The only sort of effect we've got so far is
548 *divergence* or non-termination. So the only thing thunks are useful
549 for yet is controlling whether an expression that would diverge if we
550 tried to fully evaluate it does diverge. As we consider richer
551 languages, thunks will become more useful.