1 # System F and recursive types
3 In the simply-typed lambda calculus, we write types like <code>σ
4 -> τ</code>. This looks like logical implication. We'll take
5 that resemblance seriously when we discuss the Curry-Howard
6 correspondence. In the meantime, note that types respect modus
10 Expression Type Implication
11 -----------------------------------
12 fn α -> β α ⊃ β
14 ------ ------ --------
15 (fn arg) β β
18 The implication in the right-hand column is modus ponens, of course.
20 System F was discovered by Girard (the same guy who invented Linear
21 Logic), but it was independently proposed around the same time by
22 Reynolds, who called his version the *polymorphic lambda calculus*.
23 (Reynolds was also an early player in the development of
26 System F enhances the simply-typed lambda calculus with abstraction
27 over types. In order to state System F, we'll need to adopt the
28 notational convention that "<code>x:α</code>" represents an
29 expression `x` whose type is <code>α</code>.
31 Then System F can be specified as follows (choosing notation that will
32 match up with usage in O'Caml, whose type system is based on System F):
36 types τ ::= c | 'a | τ1 -> τ2 | ∀'a. τ
37 expressions e ::= x | λx:τ. e | e1 e2 | Λ'a. e | e [τ]
39 In the definition of the types, "`c`" is a type constant (e.g., `e` or
40 `t`, or in arithmetic contexts, `N` or `Int`). "`'a`" is a type
41 variable (the tick mark just indicates that the variable ranges over
42 types rather than over values). "`τ1 -> τ2`" is the type of a
43 function from expressions of type `τ1` to expressions of type `τ2`.
44 And "`∀'a. τ`" is called a universal type, since it universally
45 quantifies over the type variable `'a`. (You can expect that in
46 `∀'a. τ`, the type `τ` will usually have at least one free occurrence
47 of `'a` somewhere inside of it.)
49 In the definition of the expressions, we have variables "`x`" as usual.
50 Abstracts "`λx:τ. e`" are similar to abstracts in the simply-typed lambda
51 calculus, except that they have their shrug variable annotated with a
52 type. Applications "`e1 e2`" are just like in the simply-typed lambda calculus.
54 In addition to variables, abstracts, and applications, we have two
55 additional ways of forming expressions: "`Λ'a. e`" is called a *type
56 abstraction*, and "`e [τ]`" is called a *type application*. The idea
57 is that <code>Λ</code> is a capital <code>λ</code>: just
58 like the lower-case <code>λ</code>, <code>Λ</code> binds
59 variables in its body, except that unlike <code>λ</code>,
60 <code>Λ</code> binds type variables instead of expression
61 variables. So in the expression
63 <code>Λ 'a (λ x:'a . x)</code>
65 the <code>Λ</code> binds the type variable `'a` that occurs in
66 the <code>λ</code> abstract. This expression is a polymorphic
67 version of the identity function. It defines one general identity
68 function that can be adapted for use with expressions of any type. In order
69 to get it ready to apply to, say, a variable of type boolean, just do
72 <code>(Λ 'a (λ x:'a . 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 α, which is
76 the type of the variable bound in the λ expression. Not
77 surprisingly, the type of this type application is a function from
80 <code>((Λ 'a (λ x:'a . x)) [t]): (b -> b)</code>
82 Likewise, if we had instantiated the type variable as an entity (base
83 type `e`), the resulting identity function would have been a function
86 <code>((Λ 'a (λ x:'a . x)) [e]): (e -> e)</code>
88 Clearly, for any choice of a type `'a`, the identity function can be
89 instantiated as a function from expresions of type `'a` to expressions
90 of type `'a`. In general, then, the type of the unapplied
91 (polymorphic) identity function is
93 <code>(Λ 'a (λ x:'a . x)): (∀ 'a . 'a -> 'a)</code>
98 We saw that the predecessor function couldn't be expressed in the
99 simply-typed lambda calculus. It can be expressed in System F,
100 however. Here is one way, coded in
101 [[Benjamin Pierce's type-checker and evaluator for
102 System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
103 part you want is called "fullpoly"):
105 N = All X . (X->X)->X->X;
106 Pair = All X . (N -> N -> X) -> X;
107 let zero = lambda X . lambda s:X->X . lambda z:X. z in
108 let snd = lambda x:N . lambda y:N . y in
109 let pair = lambda x:N . lambda y:N . lambda X . lambda z:N->N->X . z x y in
110 let suc = lambda n:N . lambda X . lambda s:X->X . lambda z:X . s (n [X] s z) in
111 let shift = lambda p:Pair . p [Pair] (lambda a:N . lambda b:N . pair (suc a) a) in
112 let pre = lambda n:N . n [Pair] shift (pair zero zero) [N] snd in
114 pre (suc (suc (suc zero)));
116 We've truncated the names of "suc(c)" and "pre(d)", since those are
117 reserved words in Pierce's system. Note that in this code, there is
118 no typographic distinction between ordinary lambda and type-level
119 lambda, though the difference is encoded in whether the variables are
120 lower case (for ordinary lambda) or upper case (for type-level
123 The key to the extra flexibility provided by System F is that we can
124 instantiate the `pair` function to return a number, as in the
125 definition of `pre`, or we can instantiate it to return an ordered
126 pair, as in the definition of the `shift` function. Because we don't
127 have to choose a single type for all uses of the pair-building
128 function, we aren't forced into a infinite regress of types.
130 [See Benjamin C. Pierce. 2002. *Types and Programming Languages*, MIT
131 Press, pp. 350--353, for `tail` for lists in System F.]
136 In fact, it is even possible to give a type for &omeage; in System F.
138 omega = lambda x:(All X. X->X) . x [All X . X->X] x in
141 Each time the internal application is performed, the type of the head
142 is chosen anew. And each time, we choose the same type as before, the
143 type of a function that takes an argument of any type and returns a
144 result of the same type...
150 OCaml has type inference: the system can often infer what the type of
151 an expression must be, based on the type of other known expressions.
153 For instance, if we type
157 The system replies with
159 val f : int -> int = <fun>
161 Since `+` is only defined on integers, it has type
164 - : int -> int -> int = <fun>
166 The parentheses are there to turn off the trick that allows the two
167 arguments of `+` to surround it in infix (for linguists, SOV) argument
173 In general, tuples with one element are identical to their one
179 though OCaml, like many systems, refuses to try to prove whether two
180 functional objects may be identical:
183 Exception: Invalid_argument "equal: functional value".
187 [Note: There is a limited way you can compare functions, using the
188 `==` operator instead of the `=` operator. Later when we discuss mutation,
189 we'll discuss the difference between these two equality operations.
190 Scheme has a similar pair, which they name `eq?` and `equal?`. In Python,
191 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
192 `(f) = f`. However, don't expect it to figure out in general when two functions
193 are equivalent. (That question is not Turing computable.)
195 # (f) == (fun x -> x + 3);;
198 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.]
202 Booleans in OCaml, and simple pattern matching
203 ----------------------------------------------
205 Where we would write `true 1 2` in our pure lambda calculus and expect
206 it to evaluate to `1`, in OCaml boolean types are not functions
207 (equivalently, they're functions that take zero arguments). Instead, selection is
208 accomplished as follows:
210 # if true then 1 else 2;;
213 The types of the `then` clause and of the `else` clause must be the
216 The `if` construction can be re-expressed by means of the following
217 pattern-matching expression:
219 match <bool expression> with true -> <expression1> | false -> <expression2>
223 # match true with true -> 1 | false -> 2;;
228 # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
234 All functions in OCaml take exactly one argument. Even this one:
236 # let f x y = x + y;;
240 Here's how to tell that `f` has been curry'd:
243 - : int -> int = <fun>
245 After we've given our `f` one argument, it returns a function that is
246 still waiting for another argument.
248 There is a special type in OCaml called `unit`. There is exactly one
249 object in this type, written `()`. So
254 Just as you can define functions that take constants for arguments
260 you can also define functions that take the unit as its argument, thus
263 val f : unit -> int = <fun>
265 Then the only argument you can possibly apply `f` to that is of the
266 correct type is the unit:
271 Now why would that be useful?
273 Let's have some fun: think of `rec` as our `Y` combinator. Then
275 # let rec f n = if (0 = n) then 1 else (n * (f (n - 1)));;
276 val f : int -> int = <fun>
280 We can't define a function that is exactly analogous to our ω.
281 We could try `let rec omega x = x x;;` what happens?
283 [Note: if you want to learn more OCaml, you might come back here someday and try:
286 val id : 'a -> 'a = <fun>
287 # let unwrap (`Wrap a) = a;;
288 val unwrap : [< `Wrap of 'a ] -> 'a = <fun>
289 # let omega ((`Wrap x) as y) = x y;;
290 val omega : [< `Wrap of [> `Wrap of 'a ] -> 'b as 'a ] -> 'b = <fun>
291 # unwrap (omega (`Wrap id)) == id;;
293 # unwrap (omega (`Wrap omega));;
294 <Infinite loop, need to control-c to interrupt>
296 But we won't try to explain this now.]
299 Even if we can't (easily) express omega in OCaml, we can do this:
301 # let rec blackhole x = blackhole x;;
303 By the way, what's the type of this function?
305 If you then apply this `blackhole` function to an argument,
309 the interpreter goes into an infinite loop, and you have to type control-c
312 Oh, one more thing: lambda expressions look like this:
316 # (fun x -> x) true;;
319 (But `(fun x -> x x)` still won't work.)
321 You may also see this:
323 # (function x -> x);;
326 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.
328 We can try our usual tricks:
330 # (fun x -> true) blackhole;;
333 OCaml declined to try to fully reduce the argument before applying the
334 lambda function. Question: Why is that? Didn't we say that OCaml is a call-by-value/eager language?
336 Remember that `blackhole` is a function too, so we can
337 reverse the order of the arguments:
339 # blackhole (fun x -> true);;
343 Now consider the following variations in behavior:
345 # let test = blackhole blackhole;;
346 <Infinite loop, need to control-c to interrupt>
348 # let test () = blackhole blackhole;;
349 val test : unit -> 'a = <fun>
352 - : unit -> 'a = <fun>
355 <Infinite loop, need to control-c to interrupt>
357 We can use functions that take arguments of type `unit` to control
358 execution. In Scheme parlance, functions on the `unit` type are called
359 *thunks* (which I've always assumed was a blend of "think" and "chunk").
361 Question: why do thunks work? We know that `blackhole ()` doesn't terminate, so why do expressions like:
363 let f = fun () -> blackhole ()
368 Bottom type, divergence
369 -----------------------
371 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:
373 type 'a option = None | Some of 'a;;
374 type 'a option = None | Some of 'a | bottom;;
376 Here are some exercises that may help better understand this. Figure out what is the type of each of the following:
384 let rec blackhole x = blackhole x in blackhole;;
386 let rec blackhole x = blackhole x in blackhole 1;;
388 let rec blackhole x = blackhole x in fun (y:int) -> blackhole y y y;;
390 let rec blackhole x = blackhole x in (blackhole 1) + 2;;
392 let rec blackhole x = blackhole x in (blackhole 1) || false;;
394 let rec blackhole x = blackhole x in 2 :: (blackhole 1);;
396 By the way, what's the type of this:
398 let rec blackhole (x:'a) : 'a = blackhole x in blackhole
401 Back to thunks: the reason you'd want to control evaluation with
402 thunks is to manipulate when "effects" happen. In a strongly
403 normalizing system, like the simply-typed lambda calculus or System F,
404 there are no "effects." In Scheme and OCaml, on the other hand, we can
405 write programs that have effects. One sort of effect is printing.
406 Another sort of effect is mutation, which we'll be looking at soon.
407 Continuations are yet another sort of effect. None of these are yet on
408 the table though. The only sort of effect we've got so far is
409 *divergence* or non-termination. So the only thing thunks are useful
410 for yet is controlling whether an expression that would diverge if we
411 tried to fully evaluate it does diverge. As we consider richer
412 languages, thunks will become more useful.