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 Exchange: &Gamma;, A, B, &Delta; |- C
 209           ---------------------------
 210           $Gamma;, B, A, &Delta; |- C
 211
 212 Contraction: &Gamma;, A, A |- B
 213              -------------------
 214              &Gamma;, A |- B
 215
 216 Weakening: &Gamma; |- B
 217            -----------------
 218            &Gamma;, A |- B
 219
 220 Logical Rules:
 221
 222 --> I:   &Gamma;, A |- B
 223          -------------------
 224          &Gamma; |- A --> B
 225
 226 --> E:   &Gamma; |- A --> B         &Gamma; |- A
 227          -----------------------------------------
 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 Exchange: &Gamma;, x:A, y:B, &Delta; |- R:C
 265           --------------------------------------
 266           &Gamma;, y:B, x:A, &Delta; |- R:C
 267
 268 Contraction: &Gamma;, x:A, x:A |- R:B
 269              --------------------------
 270              &Gamma;, x:A |- R:B
 271
 272 Weakening: &Gamma; |- R:B
 273            ---------------------
 274            &Gamma;, x:A |- R:B     [x chosen fresh]
 275
 276 Logical Rules:
 277
 278 --> I:   &Gamma;, x:A |- R:B
 279          -------------------------
 280          &Gamma; |- \xM:A --> B
 281
 282 --> E:   &Gamma; |- f:(A --> B)      &Gamma; |- x:A
 283          ---------------------------------------------
 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 Using these labeling rules, we can label the proof
 291 just given:
 292
 293 <pre>
 294 ------------  Id
 295 x:A |- x:A
 296 ---------------- Weak
 297 x:A, y:B |- x:A
 298 ------------------------- --> I
 299 x:A |- (\y.x):(B --> A)
 300 ---------------------------- --> I
 301 |- (\x y. x):A --> B --> A
 302 </pre>
 303
 304 We have derived the *K* combinator, and typed it at the same time!
 305
 306 [To do: add pairs and destructors; unit and negation...]
 307
 308 Excercise: construct a proof whose labeling is the combinator S.