Finally, we're getting consistent principle types, so we can stop.
These types should remind you of the simply-typed lambda calculus
types for Church numerals (`(o -> o) -> o -> o`) with one extra bit
-thrown in (in this case, and int).
+thrown in (in this case, an int).
So here's our type constructor for our hand-rolled lists:
So an `('a, 'b) list'` is a list containing elements of type `'a`,
where `'b` is the type of some part of the plumbing. This is more
general than an ordinary Ocaml list, but we'll see how to map them
-into Ocaml lists soon. We don't need to grasp the role of the `'b`'s
+into Ocaml lists soon. We don't need to fully grasp the role of the `'b`'s
in order to proceed to build a monad:
l'_unit (x:'a):(('a, 'b) list) = fun x -> fun f z -> f x z
Ta da!
-Just for mnemonic purposes (sneaking in an instance of eta reduction
-to the definition of unit), we can summarize the result as follows:
-
- type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b
- l'_unit x = fun f -> f x
- l'_bind u f = fun k -> u (fun x -> f x k)
-
To bad this digression, though it ties together various
elements of the course, has *no relevance whatsoever* to the topic of
-continuations.
+continuations...
Montague's PTQ treatment of DPs as generalized quantifiers
----------------------------------------------------------
belabor the construction of the bind function, the derivation is
similar to the List monad just given:
- type 'a continuation = ('a -> 'b) -> 'b
- c_unit (x:'a) = fun (p:'a -> 'b) -> p x
- c_bind (u:('a -> 'b) -> 'b) (f: 'a -> ('c -> 'd) -> 'd): ('c -> 'd) -> 'd =
- fun (k:'a -> 'b) -> u (fun (x:'a) -> f x k)
+<pre>
+type 'a continuation = ('a -> 'b) -> 'b
+c_unit (x:'a) = fun (p:'a -> 'b) -> p x
+c_bind (u:('a -> 'b) -> 'b) (f: 'a -> ('c -> 'd) -> 'd): ('c -> 'd) -> 'd =
+ fun (k:'a -> 'b) -> u (fun (x:'a) -> f x k)
+</pre>
How similar is it to the List monad? Let's examine the type
constructor and the terms from the list monad derived above:
instantiate the type of the list' monad using the Ocaml list type:
type 'a c_list = ('a -> 'a list) -> 'a list
- let c_list_unit x = fun f -> f x;;
- let c_list_bind u f = fun k -> u (fun x -> f x k);;
-Have we really discovered that lists are secretly continuations?
-Or have we merely found a way of simulating lists using list
+Have we really discovered that lists are secretly continuations? Or
+have we merely found a way of simulating lists using list
continuations? Both perspectives are valid, and we can use our
intuitions about the list monad to understand continuations, and vice
-versa. The connections will be expecially relevant when we consider
-indefinites and Hamblin semantics on the linguistic side, and
-non-determinism on the list monad side.
+versa (not to mention our intuitions about primitive recursion in
+Church numerals too). The connections will be expecially relevant
+when we consider indefinites and Hamblin semantics on the linguistic
+side, and non-determinism on the list monad side.
Refunctionalizing zippers
-------------------------