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
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:α</code>" represents an expression `x`
25 whose type is <code>α</code>.
27 Then System F can be specified as follows:
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 (α, β, 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 `α`. 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>Λ</code> is a capital <code>λ</code>: just
57 like the lower-case <code>λ</code>, <code>Λ</code> binds
58 variables in its body, except that unlike <code>λ</code>,
59 <code>Λ</code> binds type variables instead of expression
60 variables. So in the expression
62 <code>Λ α (λ x:α. x)</code>
64 the <code>Λ</code> binds the type variable `α` that occurs in
65 the <code>λ</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>(Λ α (λ 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>((Λα (λ 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
85 <code>((Λα (λ 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>(Λα (λx:α . x)): (∀α. α->α)</code>
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 ≡ ∀α.(α->α)->α->α`.
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
150 In fact, unlike in the simply-typed lambda calculus,
151 it is even possible to give a type for ω in System F.
153 <code>ω = λx:(∀α.α->α). x [∀α.α->α] x</code>
155 In order to see how this works, we'll apply ω to the identity
158 <code>ω id ≡ (λ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 ω. The definition of
162 ω 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 ω, there is no general type for Ω ≡ ω
181 ω. In fact, it turns out that no Turing complete system can be
182 strongly normalizing, from which it follows that System F is not
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
195 Ann left and Bill left.
198 Ann read and reviewed the book.
200 In English (likewise, many other languages), *and* can coordinate
201 clauses, verb phrases, determiner phrases, transitive verbs, and many
202 other phrase types. In a garden-variety simply-typed grammar, each
203 kind of conjunct has a different semantic type, and so we would need
204 an independent rule for each one. Yet there is a strong intuition
205 that the contribution of *and* remains constant across all of these
206 uses. Can we capture this using polymorphic types?
210 read, reviewed e -> e -> t
212 With these basic types, we want to say something like this:
214 and:t->t->t = λl:t. λr:t. l r false
215 and = Λα.Λβ.λl:α->β.λr:α->β.λx:α. and [β] (l x) (r x)
217 The idea is that the basic *and* (the one defined in the first line)
218 conjoins expressions of type `t`. But when *and* conjoins functional
219 types (the definition in the second line), it builds a function that
220 distributes its argument across the two conjuncts and conjoins the two
221 results. The intention is that `Ann left and slept` will evaluate to
222 `(\x.and(left x)(slept x)) ann`. Following the terminology of Partee
223 and Rooth, this strategy of defining the coordination of expressions
224 with complex types in terms of the coordination of expressions with
225 less complex types is known as Generalized Coordination.
227 But the definitions just given are not well-formed expressions in
228 System F. There are three problems. The first is that we have two
229 definitions of the same word. The intention is for one of the
230 definitions to be operative when the type of its arguments is type
231 `t`, but we have no way of conditioning evaluation on the *type* of an
232 argument. The second is that for the polymorphic definition, the term
233 *and* occurs inside of the definition. We know how to handle some
234 cases of using a function name inside of its own definition in the
235 untyped lambda calculus, but System F does not have
236 recursion. [Exercise: convince yourself that the fixed-point
237 combinator `Y` can't be typed in System F.]
239 The third problem is more subtle. The defintion as given takes two
240 types as parameters: the type of the first argument expected by each
241 conjunct, and the type of the result of applying each conjunct to an
242 argument of that type. We would like to instantiate the recursive use
243 of *and* in the definition by using the result type, so that
244 "<code>and [β]</code>" evaluates to the kind of *and* that
245 coordinates expressions of type β. But fully instantiating the
246 definition as given requires type application to a *pair* of types,
247 not to just to a single type. We want to somehow guarantee that β
248 will always itself be a complex type. This goes beyond the expressive
251 So conjunction and disjunction provide a compelling motivation for
252 polymorphism in natural language, but we don't yet have the ability to
253 build the polymorphism into a formal system.
255 And in fact, discussions of generalized coordination in the
256 linguistics literature are almost always left as a meta-level
257 generalizations over a basic simply-typed grammar. For instance, in
258 Hendriks' 1992:74 dissertation, generalized coordination is
259 implemented as a method for generating a suitable set of translation
260 rules, which are in turn expressed in a simply-typed grammar.
262 There is some work using System F to express generalizations about
263 natural language: Ponvert, Elias. 2005. Polymorphism in English Logical
264 Grammar. In *Lambda Calculus Type Theory and Natural Language*: 47--60.
266 Not incidentally, we're not aware of any programming language that
267 makes generalized coordination available, despite is naturalness and
268 ubiquity in natural language. That is, coordination in programming
269 languages is always at the sentential level. You might be able to
270 evaluate `(delete file1) and (delete file2)`, but never `delete (file1
273 We'll return to thinking about generalized coordination as we get
274 deeper into types. There will be an analysis in term of continuations
275 that will be particularly satisfying.
281 OCaml has type inference: the system can often infer what the type of
282 an expression must be, based on the type of other known expressions.
284 For instance, if we type
288 The system replies with
290 val f : int -> int = <fun>
292 Since `+` is only defined on integers, it has type
295 - : int -> int -> int = <fun>
297 The parentheses are there to turn off the trick that allows the two
298 arguments of `+` to surround it in infix (for linguists, SOV) argument
304 In general, tuples with one element are identical to their one
310 though OCaml, like many systems, refuses to try to prove whether two
311 functional objects may be identical:
314 Exception: Invalid_argument "equal: functional value".
318 [Note: There is a limited way you can compare functions, using the
319 `==` operator instead of the `=` operator. Later when we discuss mutation,
320 we'll discuss the difference between these two equality operations.
321 Scheme has a similar pair, which they name `eq?` and `equal?`. In Python,
322 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
323 `(f) = f`. However, don't expect it to figure out in general when two functions
324 are equivalent. (That question is not Turing computable.)
326 # (f) == (fun x -> x + 3);;
329 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.]
333 Booleans in OCaml, and simple pattern matching
334 ----------------------------------------------
336 Where we would write `true 1 2` in our pure lambda calculus and expect
337 it to evaluate to `1`, in OCaml boolean types are not functions
338 (equivalently, they're functions that take zero arguments). Instead, selection is
339 accomplished as follows:
341 # if true then 1 else 2;;
344 The types of the `then` clause and of the `else` clause must be the
347 The `if` construction can be re-expressed by means of the following
348 pattern-matching expression:
350 match <bool expression> with true -> <expression1> | false -> <expression2>
354 # match true with true -> 1 | false -> 2;;
359 # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
365 All functions in OCaml take exactly one argument. Even this one:
367 # let f x y = x + y;;
371 Here's how to tell that `f` has been curry'd:
374 - : int -> int = <fun>
376 After we've given our `f` one argument, it returns a function that is
377 still waiting for another argument.
379 There is a special type in OCaml called `unit`. There is exactly one
380 object in this type, written `()`. So
385 Just as you can define functions that take constants for arguments
391 you can also define functions that take the unit as its argument, thus
394 val f : unit -> int = <fun>
396 Then the only argument you can possibly apply `f` to that is of the
397 correct type is the unit:
402 Now why would that be useful?
404 Let's have some fun: think of `rec` as our `Y` combinator. Then
406 # let rec f n = if (0 = n) then 1 else (n * (f (n - 1)));;
407 val f : int -> int = <fun>
411 We can't define a function that is exactly analogous to our ω.
412 We could try `let rec omega x = x x;;` what happens?
414 [Note: if you want to learn more OCaml, you might come back here someday and try:
417 val id : 'a -> 'a = <fun>
418 # let unwrap (`Wrap a) = a;;
419 val unwrap : [< `Wrap of 'a ] -> 'a = <fun>
420 # let omega ((`Wrap x) as y) = x y;;
421 val omega : [< `Wrap of [> `Wrap of 'a ] -> 'b as 'a ] -> 'b = <fun>
422 # unwrap (omega (`Wrap id)) == id;;
424 # unwrap (omega (`Wrap omega));;
425 <Infinite loop, need to control-c to interrupt>
427 But we won't try to explain this now.]
430 Even if we can't (easily) express omega in OCaml, we can do this:
432 # let rec blackhole x = blackhole x;;
434 By the way, what's the type of this function?
436 If you then apply this `blackhole` function to an argument,
440 the interpreter goes into an infinite loop, and you have to type control-c
443 Oh, one more thing: lambda expressions look like this:
447 # (fun x -> x) true;;
450 (But `(fun x -> x x)` still won't work.)
452 You may also see this:
454 # (function x -> x);;
457 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.
459 We can try our usual tricks:
461 # (fun x -> true) blackhole;;
464 OCaml declined to try to fully reduce the argument before applying the
465 lambda function. Question: Why is that? Didn't we say that OCaml is a call-by-value/eager language?
467 Remember that `blackhole` is a function too, so we can
468 reverse the order of the arguments:
470 # blackhole (fun x -> true);;
474 Now consider the following variations in behavior:
476 # let test = blackhole blackhole;;
477 <Infinite loop, need to control-c to interrupt>
479 # let test () = blackhole blackhole;;
480 val test : unit -> 'a = <fun>
483 - : unit -> 'a = <fun>
486 <Infinite loop, need to control-c to interrupt>
488 We can use functions that take arguments of type `unit` to control
489 execution. In Scheme parlance, functions on the `unit` type are called
490 *thunks* (which I've always assumed was a blend of "think" and "chunk").
492 Question: why do thunks work? We know that `blackhole ()` doesn't terminate, so why do expressions like:
494 let f = fun () -> blackhole ()
499 Bottom type, divergence
500 -----------------------
502 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:
504 type 'a option = None | Some of 'a;;
505 type 'a option = None | Some of 'a | bottom;;
507 Here are some exercises that may help better understand this. Figure out what is the type of each of the following:
515 let rec blackhole x = blackhole x in blackhole;;
517 let rec blackhole x = blackhole x in blackhole 1;;
519 let rec blackhole x = blackhole x in fun (y:int) -> blackhole y y y;;
521 let rec blackhole x = blackhole x in (blackhole 1) + 2;;
523 let rec blackhole x = blackhole x in (blackhole 1) || false;;
525 let rec blackhole x = blackhole x in 2 :: (blackhole 1);;
527 By the way, what's the type of this:
529 let rec blackhole (x:'a) : 'a = blackhole x in blackhole
532 Back to thunks: the reason you'd want to control evaluation with
533 thunks is to manipulate when "effects" happen. In a strongly
534 normalizing system, like the simply-typed lambda calculus or System F,
535 there are no "effects." In Scheme and OCaml, on the other hand, we can
536 write programs that have effects. One sort of effect is printing.
537 Another sort of effect is mutation, which we'll be looking at soon.
538 Continuations are yet another sort of effect. None of these are yet on
539 the table though. The only sort of effect we've got so far is
540 *divergence* or non-termination. So the only thing thunks are useful
541 for yet is controlling whether an expression that would diverge if we
542 tried to fully evaluate it does diverge. As we consider richer
543 languages, thunks will become more useful.