1 [[!toc levels=2]]
3 # System F: the polymorphic lambda calculus
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.
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.)
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.
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>.
27 Then System F can be specified as follows:
29         System F:
30         ---------
31         types       τ ::= c | α | τ1 -> τ2 | ∀α.τ
32         expressions e ::= x | λx:τ.e | e1 e2 | Λα.e | e [τ]
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.
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.
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
62 <code>&Lambda; α (&lambda; x:α. x)</code>
64 the <code>&Lambda;</code> binds the type variable `α` that occurs in
65 the <code>&lambda;</code> abstract.
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:
72 <code>(&Lambda; α (&lambda; x:α. x)) [t]</code>
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:
79 <code>((&Lambda;α (&lambda; x:α . x)) [t]): (b->b)</code>
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`:
85 <code>((&Lambda;α (&lambda; x:α. x)) [e]): (e->e)</code>
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
92 <code>(&Lambda;α (&lambda;x:α . x)): (&forall;α. α->α)</code>
94 Pred in System F
95 ----------------
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:
101     let N = ∀α.(α->α)->α->α in
102     let Pair = (N->N->N)->N in
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
112     pre (suc (suc (suc zero)));
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.]
121 Exercise: convince yourself that `zero` has type `N`.
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.
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.
144 [See Benjamin C. Pierce. 2002. *Types and Programming Languages*, MIT
145 Press, chapter 23.]
147 Typing &omega;
148 --------------
150 In fact, unlike in the simply-typed lambda calculus,
151 it is even possible to give a type for &omega; in System F.
153 <code>&omega; = λx:(∀α.α->α). x [∀α.α->α] x</code>
155 In order to see how this works, we'll apply &omega; to the identity
156 function.
158 <code>&omega; id &equiv; (λx:(∀α.α->α). x [∀α.α->α] x) (Λα.λx:α.x)</code>
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.
168 So in System F, unlike in the simply-typed lambda calculus, it *is*
169 possible for a function to apply to itself!
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.
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.
186 ## Polymorphism in natural language
188 Is the simply-typed lambda calclus enough for analyzing natural
189 language, or do we need polymorphic types? Or something even more expressive?
191 The classic case study motivating polymorphism in natural language
192 comes from coordination.  (The locus classicus is Partee and Rooth
193 1983.)
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)
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.
209 Can we capture this using polymorphic types?
211     Ann, Bill      e
212     left, slept    e -> t
213     read, reviewed e -> e -> t
215 With these basic types, we want to say something like this:
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)
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*.
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
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`.
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.
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.
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.
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.
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)`.
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.
277 #Types in OCaml
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.
283 For instance, if we type
285     # let f x = x + 3;;
287 The system replies with
289     val f : int -> int = <fun>
291 Since `+` is only defined on integers, it has type
293      # (+);;
294      - : int -> int -> int = <fun>
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,
300     # 3 + 4 = (+) 3 4;;
301     - : bool = true
303 In general, tuples with one element are identical to their one
304 element:
306     # (3) = 3;;
307     - : bool = true
309 though OCaml, like many systems, refuses to try to prove whether two
310 functional objects may be identical:
312     # (f) = f;;
313     Exception: Invalid_argument "equal: functional value".
315 Oh well.
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.)
325         # (f) == (fun x -> x + 3);;
326         - : bool = false
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.]
332 Booleans in OCaml, and simple pattern matching
333 ----------------------------------------------
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:
340     # if true then 1 else 2;;
341     - : int = 1
343 The types of the `then` clause and of the `else` clause must be the
344 same.
346 The `if` construction can be re-expressed by means of the following
347 pattern-matching expression:
349     match <bool expression> with true -> <expression1> | false -> <expression2>
351 That is,
353     # match true with true -> 1 | false -> 2;;
354     - : int = 1
356 Compare with
358     # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
359     - : int = 9
361 Unit and thunks
362 ---------------
364 All functions in OCaml take exactly one argument.  Even this one:
366     # let f x y = x + y;;
367     # f 2 3;;
368     - : int = 5
370 Here's how to tell that `f` has been curry'd:
372     # f 2;;
373     - : int -> int = <fun>
375 After we've given our `f` one argument, it returns a function that is
376 still waiting for another argument.
378 There is a special type in OCaml called `unit`.  There is exactly one
379 object in this type, written `()`.  So
381     # ();;
382     - : unit = ()
384 Just as you can define functions that take constants for arguments
386     # let f 2 = 3;;
387     # f 2;;
388     - : int = 3;;
390 you can also define functions that take the unit as its argument, thus
392     # let f () = 3;;
393     val f : unit -> int = <fun>
395 Then the only argument you can possibly apply `f` to that is of the
396 correct type is the unit:
398     # f ();;
399     - : int = 3
401 Now why would that be useful?
403 Let's have some fun: think of `rec` as our `Y` combinator.  Then
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
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?
413 [Note: if you want to learn more OCaml, you might come back here someday and try:
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>
426 But we won't try to explain this now.]
429 Even if we can't (easily) express omega in OCaml, we can do this:
431     # let rec blackhole x = blackhole x;;
433 By the way, what's the type of this function?
435 If you then apply this `blackhole` function to an argument,
437     # blackhole 3;;
439 the interpreter goes into an infinite loop, and you have to type control-c
440 to break the loop.
442 Oh, one more thing: lambda expressions look like this:
444     # (fun x -> x);;
445     - : 'a -> 'a = <fun>
446     # (fun x -> x) true;;
447     - : bool = true
449 (But `(fun x -> x x)` still won't work.)
451 You may also see this:
453         # (function x -> x);;
454         - : 'a -> 'a = <fun>
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.
458 We can try our usual tricks:
460     # (fun x -> true) blackhole;;
461     - : bool = true
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?
466 Remember that `blackhole` is a function too, so we can
467 reverse the order of the arguments:
469     # blackhole (fun x -> true);;
471 Infinite loop.
473 Now consider the following variations in behavior:
475     # let test = blackhole blackhole;;
476     <Infinite loop, need to control-c to interrupt>
478     # let test () = blackhole blackhole;;
479     val test : unit -> 'a = <fun>
481     # test;;
482     - : unit -> 'a = <fun>
484     # test ();;
485     <Infinite loop, need to control-c to interrupt>
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").
491 Question: why do thunks work? We know that `blackhole ()` doesn't terminate, so why do expressions like:
493         let f = fun () -> blackhole ()
494         in true
496 terminate?
498 Bottom type, divergence
499 -----------------------
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:
503         type 'a option = None | Some of 'a;;
504         type 'a option = None | Some of 'a | bottom;;
506 Here are some exercises that may help better understand this. Figure out what is the type of each of the following:
508         fun x y -> y;;
510         fun x (y:int) -> y;;
512         fun x y : int -> y;;
514         let rec blackhole x = blackhole x in blackhole;;
516         let rec blackhole x = blackhole x in blackhole 1;;
518         let rec blackhole x = blackhole x in fun (y:int) -> blackhole y y y;;
520         let rec blackhole x = blackhole x in (blackhole 1) + 2;;
522         let rec blackhole x = blackhole x in (blackhole 1) || false;;
524         let rec blackhole x = blackhole x in 2 :: (blackhole 1);;
526 By the way, what's the type of this:
528         let rec blackhole (x:'a) : 'a = blackhole x in blackhole
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.