Higher Order Fun

(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.