if we can gain some insight into the details of the List monad. Let's
choose type constructor that we can peer into, using some of the
technology we built up so laboriously during the first half of the
-course. We're going to use type 3 lists, partly because I know
-they'll give the result I want, but also because they're the coolest.
+course. We're going to use type 3 lists, partly because we know
+they'll give the result we want, but also because they're the coolest.
These were the lists that made lists look like Church numerals with
extra bits embdded in them:
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)
+ 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
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
-------------------------