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)
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, however.
101 [See Benjamin C. Pierce. 2002. *Types and Programming Languages*, MIT
102 Press, pp. 350--353, for `tail` for lists in System F.]
108 OCaml has type inference: the system can often infer what the type of
109 an expression must be, based on the type of other known expressions.
111 For instance, if we type
115 The system replies with
117 val f : int -> int = <fun>
119 Since `+` is only defined on integers, it has type
122 - : int -> int -> int = <fun>
124 The parentheses are there to turn off the trick that allows the two
125 arguments of `+` to surround it in infix (for linguists, SOV) argument
131 In general, tuples with one element are identical to their one
137 though OCaml, like many systems, refuses to try to prove whether two
138 functional objects may be identical:
141 Exception: Invalid_argument "equal: functional value".
145 [Note: There is a limited way you can compare functions, using the
146 `==` operator instead of the `=` operator. Later when we discuss mutation,
147 we'll discuss the difference between these two equality operations.
148 Scheme has a similar pair, which they name `eq?` and `equal?`. In Python,
149 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
150 `(f) = f`. However, don't expect it to figure out in general when two functions
151 are equivalent. (That question is not Turing computable.)
153 # (f) == (fun x -> x + 3);;
156 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.]
160 Booleans in OCaml, and simple pattern matching
161 ----------------------------------------------
163 Where we would write `true 1 2` in our pure lambda calculus and expect
164 it to evaluate to `1`, in OCaml boolean types are not functions
165 (equivalently, they're functions that take zero arguments). Instead, selection is
166 accomplished as follows:
168 # if true then 1 else 2;;
171 The types of the `then` clause and of the `else` clause must be the
174 The `if` construction can be re-expressed by means of the following
175 pattern-matching expression:
177 match <bool expression> with true -> <expression1> | false -> <expression2>
181 # match true with true -> 1 | false -> 2;;
186 # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
192 All functions in OCaml take exactly one argument. Even this one:
194 # let f x y = x + y;;
198 Here's how to tell that `f` has been curry'd:
201 - : int -> int = <fun>
203 After we've given our `f` one argument, it returns a function that is
204 still waiting for another argument.
206 There is a special type in OCaml called `unit`. There is exactly one
207 object in this type, written `()`. So
212 Just as you can define functions that take constants for arguments
218 you can also define functions that take the unit as its argument, thus
221 val f : unit -> int = <fun>
223 Then the only argument you can possibly apply `f` to that is of the
224 correct type is the unit:
229 Now why would that be useful?
231 Let's have some fun: think of `rec` as our `Y` combinator. Then
233 # let rec f n = if (0 = n) then 1 else (n * (f (n - 1)));;
234 val f : int -> int = <fun>
238 We can't define a function that is exactly analogous to our ω.
239 We could try `let rec omega x = x x;;` what happens?
241 [Note: if you want to learn more OCaml, you might come back here someday and try:
244 val id : 'a -> 'a = <fun>
245 # let unwrap (`Wrap a) = a;;
246 val unwrap : [< `Wrap of 'a ] -> 'a = <fun>
247 # let omega ((`Wrap x) as y) = x y;;
248 val omega : [< `Wrap of [> `Wrap of 'a ] -> 'b as 'a ] -> 'b = <fun>
249 # unwrap (omega (`Wrap id)) == id;;
251 # unwrap (omega (`Wrap omega));;
252 <Infinite loop, need to control-c to interrupt>
254 But we won't try to explain this now.]
257 Even if we can't (easily) express omega in OCaml, we can do this:
259 # let rec blackhole x = blackhole x;;
261 By the way, what's the type of this function?
263 If you then apply this `blackhole` function to an argument,
267 the interpreter goes into an infinite loop, and you have to type control-c
270 Oh, one more thing: lambda expressions look like this:
274 # (fun x -> x) true;;
277 (But `(fun x -> x x)` still won't work.)
279 You may also see this:
281 # (function x -> x);;
284 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.
286 We can try our usual tricks:
288 # (fun x -> true) blackhole;;
291 OCaml declined to try to fully reduce the argument before applying the
292 lambda function. Question: Why is that? Didn't we say that OCaml is a call-by-value/eager language?
294 Remember that `blackhole` is a function too, so we can
295 reverse the order of the arguments:
297 # blackhole (fun x -> true);;
301 Now consider the following variations in behavior:
303 # let test = blackhole blackhole;;
304 <Infinite loop, need to control-c to interrupt>
306 # let test () = blackhole blackhole;;
307 val test : unit -> 'a = <fun>
310 - : unit -> 'a = <fun>
313 <Infinite loop, need to control-c to interrupt>
315 We can use functions that take arguments of type `unit` to control
316 execution. In Scheme parlance, functions on the `unit` type are called
317 *thunks* (which I've always assumed was a blend of "think" and "chunk").
319 Question: why do thunks work? We know that `blackhole ()` doesn't terminate, so why do expressions like:
321 let f = fun () -> blackhole ()
326 Bottom type, divergence
327 -----------------------
329 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:
331 type 'a option = None | Some of 'a;;
332 type 'a option = None | Some of 'a | bottom;;
334 Here are some exercises that may help better understand this. Figure out what is the type of each of the following:
342 let rec blackhole x = blackhole x in blackhole;;
344 let rec blackhole x = blackhole x in blackhole 1;;
346 let rec blackhole x = blackhole x in fun (y:int) -> blackhole y y y;;
348 let rec blackhole x = blackhole x in (blackhole 1) + 2;;
350 let rec blackhole x = blackhole x in (blackhole 1) || false;;
352 let rec blackhole x = blackhole x in 2 :: (blackhole 1);;
354 By the way, what's the type of this:
356 let rec blackhole (x:'a) : 'a = blackhole x in blackhole
359 Back to thunks: the reason you'd want to control evaluation with
360 thunks is to manipulate when "effects" happen. In a strongly
361 normalizing system, like the simply-typed lambda calculus or System F,
362 there are no "effects." In Scheme and OCaml, on the other hand, we can
363 write programs that have effects. One sort of effect is printing.
364 Another sort of effect is mutation, which we'll be looking at soon.
365 Continuations are yet another sort of effect. None of these are yet on
366 the table though. The only sort of effect we've got so far is
367 *divergence* or non-termination. So the only thing thunks are useful
368 for yet is controlling whether an expression that would diverge if we
369 tried to fully evaluate it does diverge. As we consider richer
370 languages, thunks will become more useful.