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