1 # System F and recursive types
3 In the simply-typed lambda calculus, we write types like <code>&sigma;
4 -> &tau;</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
7 ponens:
9 <pre>
10 Expression    Type      Implication
11 -----------------------------------
12 fn            &alpha; -> &beta;    &alpha; &sup; &beta;
13 arg           &alpha;         &alpha;
14 ------        ------    --------
15 (fn arg)      &beta;         &beta;
16 </pre>
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
24 continuations.)
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:&alpha;</code>" represents an
29 expression `x` whose type is <code>&alpha;</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):
34         System F:
35         ---------
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>&Lambda;</code> is a capital <code>&lambda;</code>: just
58 like the lower-case <code>&lambda;</code>, <code>&Lambda;</code> binds
59 variables in its body, except that unlike <code>&lambda;</code>,
60 <code>&Lambda;</code> binds type variables instead of expression
61 variables.  So in the expression
63 <code>&Lambda; 'a (&lambda; x:'a . x)</code>
65 the <code>&Lambda;</code> binds the type variable `'a` that occurs in
66 the <code>&lambda;</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
70 this:
72 <code>(&Lambda; 'a (&lambda; 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 &alpha;, which is
76 the type of the variable bound in the &lambda; expression.  Not
77 surprisingly, the type of this type application is a function from
78 Booleans to Booleans:
80 <code>((&Lambda; 'a (&lambda; 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
84 of type `e -> e`:
86 <code>((&Lambda; 'a (&lambda; 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>(&Lambda; 'a (&lambda; x:'a . x)): (&forall; 'a . 'a -> 'a)</code>
95 Pred in System F
96 ----------------
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.]
105 Types in OCaml
106 --------------
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
113     # let f x = x + 3;;
115 The system replies with
117     val f : int -> int = <fun>
119 Since `+` is only defined on integers, it has type
121      # (+);;
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
126 order. That is,
128     # 3 + 4 = (+) 3 4;;
129     - : bool = true
131 In general, tuples with one element are identical to their one
132 element:
134     # (3) = 3;;
135     - : bool = true
137 though OCaml, like many systems, refuses to try to prove whether two
138 functional objects may be identical:
140     # (f) = f;;
141     Exception: Invalid_argument "equal: functional value".
143 Oh well.
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);;
154         - : bool = false
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;;
169     - : int = 1
171 The types of the `then` clause and of the `else` clause must be the
172 same.
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>
179 That is,
181     # match true with true -> 1 | false -> 2;;
182     - : int = 1
184 Compare with
186     # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
187     - : int = 9
189 Unit and thunks
190 ---------------
192 All functions in OCaml take exactly one argument.  Even this one:
194     # let f x y = x + y;;
195     # f 2 3;;
196     - : int = 5
198 Here's how to tell that `f` has been curry'd:
200     # f 2;;
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
209     # ();;
210     - : unit = ()
212 Just as you can define functions that take constants for arguments
214     # let f 2 = 3;;
215     # f 2;;
216     - : int = 3;;
218 you can also define functions that take the unit as its argument, thus
220     # let f () = 3;;
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:
226     # f ();;
227     - : int = 3
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>
235     # f 5;;
236     - : int = 120
238 We can't define a function that is exactly analogous to our &omega;.
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:
243         # let id x = x;;
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;;
250         - : bool = true
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,
265     # blackhole 3;;
267 the interpreter goes into an infinite loop, and you have to type control-c
268 to break the loop.
270 Oh, one more thing: lambda expressions look like this:
272     # (fun x -> x);;
273     - : 'a -> 'a = <fun>
274     # (fun x -> x) true;;
275     - : bool = true
277 (But `(fun x -> x x)` still won't work.)
279 You may also see this:
281         # (function x -> x);;
282         - : 'a -> 'a = <fun>
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;;
289     - : bool = true
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);;
299 Infinite loop.
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>
309     # test;;
310     - : unit -> 'a = <fun>
312     # test ();;
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 ()
322         in true
324 terminate?
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:
336         fun x y -> y;;
338         fun x (y:int) -> y;;
340         fun x y : int -> y;;
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.