(the serious title of this post is "First-Class Modules Encode Type-Safe Reification of Types" or some such) After reading Kiselyov and Yallop's "First-class modules: hidden power and tantalizing promises", I wanted to understand how first-class modules relate to higher order types. They state that [f]irst-class modules — first-class functors — permit type constructor abstraction and polymorphism
. They show one such use of constructor parametricity; I wanted to try another by encoding Haskell's canonical type class. Yes, I'm talking about Monad
! Here it is:
module type MONAD = sig type 'a t val return : 'a -> 'a t val (>>=) : 'a t -> ('a -> 'b t) -> 'b t val fail : 'a t end
The idea Oleg and Jeremy outline in "Generics for the OCaml masses" is to reify a type constructor α t
as a module that wraps it together with its type parameter. Since a type constructor bound in a module type (in this case α MONAD.t
) "cannot escape" for soundness' sake, it must be packed and unpacked. In effect this constitutes a higher-order existential type:
module type Monad = sig type a module Repr (M : MONAD) : sig val extract : a M.t end end
Here it is crucial to see that the extraction is entirely dependent on the actual "interpretation" (the term originally used by Oleg and Jeremy) of the type given by its definition in the module parameterizing it. Uses of these packed representations of first-class constructors must ensure that the interpretation is consistent (something that in Haskell is assured by the use of a type class parameter, as in Monad m ⇒ …
). The use of a type synonym restores polymorphism:
type 'a monad = (module Monad with type a = 'a)
In order to enable concrete instances of MONAD
to "display their wares" so to speak, it is convenient to let them unpack these representations by themselves:
module Make (M : MONAD) = struct include M let run (type s) (mx : s monad) : s t = let module MX = (val mx : Monad with type a = s) in let module RX = MX.Repr(M) in RX.extract end
Given a concrete constructor M.t
, the σ monad
is let
-bound as a module, its representation under M
is obtained and the corresponding value extracted. The same pattern recurs in the following genuinely higher-kinded functions, of which return
is the simplest:
let return : 'a . 'a -> 'a monad = fun (type s) x -> (module struct type a = s module Repr (M : MONAD) = struct let extract = M.return x end end : Monad with type a = s)
Note that the result type is α monad
, that is, a bona-fide module. Note also that the representation of value x under the monad M
is exactly M.return x
. So far, no complications. Now for something completely different:
let (>>=) : 'a . 'a monad -> ('a -> 'b monad) -> 'b monad = fun (type s) (type t) mx f -> (module struct type a = t type res = t module Repr (M : MONAD) = struct let extract = let module MX = (val mx : Monad with type a = s) in let module RX = MX.Repr(M) in M.(RX.extract >>= fun x -> let my = f x in let module MY = (val my : Monad with type a = res) in let module RY = MY.Repr(M) in RY.extract ) end end : Monad with type a = t)
Given mx of module type Monad with type a = σ
, its representation under M is extracted and monadically bound to f, which produces a value my of module type Monad with type a = τ
, under exactly the same monadic interpretation given by M. A technicality: since the modules are abstract, they are generative (every name is fresh); hence to force the sharing of type τ between my and the result value I need to rebind it with a unique name res that can be shared across scopes. Now the next thing is a bit disturbing:
let fail : 'a . 'a monad = fun (type s) -> (module struct type a = s module Repr (M : MONAD) = struct let extract = M.fail end end : Monad with type a = s)
Really, is that a type-level function‽ Actually no, the syntax fun (type σ) → …
binds the type σ locally in the body of the function (I'd find it clearer if the syntax were let type s = … in …
, provided that no constructor escapes. Maybe in OCaml 3.14?) That's it! All that remains is to write monadic functions as if they were given the necessary type class:
let liftM f mx = mx >>= fun x -> return (f x) let (>>) mx my = mx >>= fun _ -> my let guard p = if p then return () else fail
(exercise: define the obvious join
and verify that it really has type α monad monad → α monad
. Bonus points: expand its definition). The usage with concrete instances of MONAD
is surprisingly straightforward. For instance, given the standard:
module OptionM = Make(struct type 'a t = 'a option let return x = Some x let (>>=) mx f = match mx with None -> None | Some x -> f x let fail = None end) module ListM = Make(struct type 'a t = 'a list let return x = [x] let (>>=) mx f = List.(concat (map f mx)) let fail = [] end)
The following deceptively simple code just works:
# let v = liftM succ (return 3) >>= fun x -> return (succ x);; val v : int monad = <module> # OptionM.run v ;; - : int OptionM.t = Some 5 # ListM.run v ;; - : int ListM.t = [5]
The monadic computation v exists completely independently of the computational interpretation under which it is evaluated! Note that this interpretation is selected at runtime, not at compile-time; if it weren't for the differing types, the relevant run
could be a higher-order parameter to a generic function.
2 comments:
Hi, I saw a partial blog entry about benchmarking asynchronous IO from you on Ocaml Planet. And your own blog doesn't have the entry at all. So I assume something got lost somewhere. Could you blog again about your results please.
That post was in substantial error, so I retracted it. I'm sorry for the inconvenience.
Post a Comment