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