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
 174 Curry-Howard, take 1
 175 --------------------
 176
 177 We will return to the Curry-Howard correspondence a number of times
 178 during this course.  It expresses a deep connection between logic,
 179 types, and computation.  Today we'll discuss how the simply-typed
 180 lambda calculus corresponds to intuitionistic logic.  This naturally
 181 give rise to the question of what sort of computation classical logic
 182 corresponds to---as we'll see later, the answer involves continuations.
 183
 184 So at this point we have the simply-typed lambda calculus: a set of
 185 ground types, a set of functional types, and some typing rules, given
 186 roughly as follows:
 187
 188 If a variable `x` has type &sigma; and term `M` has type &tau;, then
 189 the abstract `\xM` has type &sigma; `-->` &tau;.
 190
 191 If a term `M` has type &sigma; `-->` &tau;, and a term `N` has type
 192 &sigma;, then the application `MN` has type &tau;.
 193
 194 These rules are clearly obverses of one another: the functional types
 195 that abstract builds up are taken apart by application.
 196
 197 The next step in making sense out of the Curry-Howard corresponence is
 198 to present a logic.  It will be a part of intuitionistic logic.  We'll
 199 start with the implicational fragment (that is, the part of
 200 intuitionistic logic that only involves axioms and implications):
 201
 202 <pre>
 203 Axiom: ---------
 204         A |- A
 205
 206 Structural Rules:
 207
 208           &Gamma;, A, B, &Delta; |- C
 209 Exchange: ---------------------------
 210           &Gamma;, B, A, &Delta; |- C
 211
 212              &Gamma;, A, A |- B
 213 Contraction: -------------------
 214              &Gamma;, A |- B
 215
 216            &Gamma; |- B
 217 Weakening: -----------------
 218            &Gamma;, A |- B
 219
 220 Logical Rules:
 221
 222          &Gamma;, A |- B
 223 --> I:   -------------------
 224          &Gamma; |- A --> B
 225
 226          &Gamma; |- A --> B         &Gamma; |- A
 227 --> E:   -----------------------------------
 228          &Gamma; |- B
 229 </pre>
 230
 231 `A`, `B`, etc. are variables over formulas.
 232 &Gamma;, &Delta;, etc. are variables over (possibly empty) sequences
 233 of formulas.  &Gamma; `|- A` is a sequent, and is interpreted as
 234 claiming that if each of the formulas in &Gamma; is true, then `A`
 235 must also be true.
 236
 237 This logic allows derivations of theorems like the following:
 238
 239 <pre>
 240 -------  Id
 241 A |- A
 242 ---------- Weak
 243 A, B |- A
 244 ------------- --> I
 245 A |- B --> A
 246 ----------------- --> I
 247 |- A --> B --> A
 248 </pre>
 249
 250 Should remind you of simple types.  (What was `A --> B --> A` the type
 251 of again?)
 252
 253 The easy way to grasp the Curry-Howard correspondence is to *label*
 254 the proofs.  Since we wish to establish a correspondence between this
 255 logic and the lambda calculus, the labels will all be terms from the
 256 simply-typed lambda calculus.  Here are the labeling rules:
 257
 258 <pre>
 259 Axiom: -----------
 260        x:A |- x:A
 261
 262 Structural Rules:
 263
 264           &Gamma;, x:A, y:B, &Delta; |- R:C
 265 Exchange: -------------------------------
 266           &Gamma;, y:B, x:A, &Delta; |- R:C
 267
 268              &Gamma;, x:A, x:A |- R:B
 269 Contraction: --------------------------
 270              &Gamma;, x:A |- R:B
 271
 272            &Gamma; |- R:B
 273 Weakening: ---------------------
 274            &Gamma;, x:A |- R:B     [x chosen fresh]
 275
 276 Logical Rules:
 277
 278          &Gamma;, x:A |- R:B
 279 --> I:   -------------------------
 280          &Gamma; |- \xM:A --> B
 281
 282          &Gamma; |- f:(A --> B)      &Gamma; |- x:A
 283 --> E:   -------------------------------------
 284          &Gamma; |- (fx):B
 285 </pre>
 286
 287 In these labeling rules, if a sequence &Gamma; in a premise contains
 288 labeled formulas, those labels remain unchanged in the conclusion.
 289
 290 What is means for a variable `x` to be chosen *fresh* is that
 291 `x` must be distinct from any other variable in any of the labels
 292 used in the proof.
 293
 294 Using these labeling rules, we can label the proof
 295 just given:
 296
 297 <pre>
 298 ------------  Id
 299 x:A |- x:A
 300 ---------------- Weak
 301 x:A, y:B |- x:A
 302 ------------------------- --> I
 303 x:A |- (\y.x):(B --> A)
 304 ---------------------------- --> I
 305 |- (\x y. x):A --> B --> A
 306 </pre>
 307
 308 We have derived the *K* combinator, and typed it at the same time!
 309
 310 Need a proof that involves application, and a proof with cut that will
 311 show beta reduction, so "normal" proof.
 312
 313 [To do: add pairs and destructors; unit and negation...]
 314
 315 Excercise: construct a proof whose labeling is the combinator S.