221e02077378f650111c0facbaea9cc9d649eb23
[lambda.git] / week6.mdwn
1 [[!toc]]
2
3 Types, OCAML
4 ------------
5
6 OCAML has type inference: the system can often infer what the type of
7 an expression must be, based on the type of other known expressions.
8
9 For instance, if we type 
10
11     # let f x = x + 3;;
12
13 The system replies with 
14
15     val f : int -> int = <fun>
16
17 Since `+` is only defined on integers, it has type
18
19      # (+);;
20      - : int -> int -> int = <fun>
21
22 The parentheses are there to turn off the trick that allows the two
23 arguments of `+` to surround it in infix (for linguists, SOV) argument
24 order. That is,
25
26     # 3 + 4 = (+) 3 4;;
27     - : bool = true
28
29 In general, tuples with one element are identical to their one
30 element:
31
32     # (3) = 3;;
33     - : bool = true
34
35 though OCAML, like many systems, refuses to try to prove whether two
36 functional objects may be identical:
37
38     # (f) = f;;
39     Exception: Invalid_argument "equal: functional value".
40
41 Oh well.
42
43
44 Booleans in OCAML, and simple pattern matching
45 ----------------------------------------------
46
47 Where we would write `true 1 2` in our pure lambda calculus and expect
48 it to evaluate to `1`, in OCAML boolean types are not functions
49 (equivalently, are functions that take zero arguments).  Selection is
50 accomplished as follows:
51
52     # if true then 1 else 2;;
53     - : int = 1
54
55 The types of the `then` clause and of the `else` clause must be the
56 same.
57
58 The `if` construction can be re-expressed by means of the following
59 pattern-matching expression:
60
61     match <bool expression> with true -> <expression1> | false -> <expression2>
62
63 That is,
64
65     # match true with true -> 1 | false -> 2;;
66     - : int = 1
67
68 Compare with 
69
70     # match 3 with 1 -> 1 | 2 -> 4 | 3 -> 9;;
71     - : int = 9
72
73 Unit and thunks
74 ---------------
75
76 All functions in OCAML take exactly one argument.  Even this one:
77
78     # let f x y = x + y;;
79     # f 2 3;;
80     - : int = 5
81
82 Here's how to tell that `f` has been curry'd:
83
84     # f 2;;
85     - : int -> int = <fun>
86
87 After we've given our `f` one argument, it returns a function that is
88 still waiting for another argument.
89
90 There is a special type in OCAML called `unit`.  There is exactly one
91 object in this type, written `()`.  So
92
93     # ();;
94     - : unit = ()
95
96 Just as you can define functions that take constants for arguments
97
98     # let f 2 = 3;;
99     # f 2;;
100     - : int = 3;;
101
102 you can also define functions that take the unit as its argument, thus
103
104     # let f () = 3;;
105     val f : unit -> int = <fun>
106
107 Then the only argument you can possibly apply `f` to that is of the
108 correct type is the unit:
109
110     # f ();;
111     - : int = 3
112
113 Let's have some fn: think of `rec` as our `Y` combinator.  Then
114
115     # let rec f n = if (0 = n) then 1 else (n * (f (n - 1)));; 
116     val f : int -> int = <fun>
117     # f 5;;
118     - : int = 120
119
120 We can't define a function that is exactly analogous to our &omega;.
121 We could try `let rec omega x = x x;;` what happens?  However, we can
122 do this:
123
124     # let rec omega x = omega x;;
125
126 By the way, what's the type of this function?
127 If you then apply this omega to an argument,
128
129     # omega 3;;
130
131 the interpreter goes into an infinite loop, and you have to control-C
132 to break the loop.
133
134 Oh, one more thing: lambda expressions look like this:
135
136     # (fun x -> x);;
137     - : 'a -> 'a = <fun>
138     # (fun x -> x) true;;
139     - : bool = true
140
141 (But `(fun x -> x x)` still won't work.)
142
143 So we can try our usual tricks:
144
145     # (fun x -> true) omega;;
146     - : bool = true
147
148 OCAML declined to try to evaluate the argument before applying the
149 functor.  But remember that `omega` is a function too, so we can
150 reverse the order of the arguments:
151
152     # omega (fun x -> true);;
153
154 Infinite loop.
155
156 Now consider the following variations in behavior:
157
158     # let test = omega omega;;
159     [Infinite loop, need to control c out]
160
161     # let test () = omega omega;;
162     val test : unit -> 'a = <fun>
163
164     # test;;
165     - : unit -> 'a = <fun>
166
167     # test ();;
168     [Infinite loop, need to control c out]
169
170 We can use functions that take arguments of type unit to control
171 execution.  In Scheme parlance, functions on the unit type are called
172 *thunks* (which I've always assumed was a blend of "think" and "chunk").
173