Free Monads - SML

Just to review, we have the following signature for monads in Standard ML:

signature MONAD = sig
  include FUNCTOR;
  val return : 'a -> 'a t;
  val bind : 'a t -> ('a -> 'b t) -> 'b t;
  val join : 'a t t -> 'a t;
end;

We may or may not need the exec function to perform the computation abstracted away by the monad.

A free monad will take a Functor, and turn it into a monad. The Functor is kept as a field of the structure.

Intuitively, a free monad is generated by a "join" operation (or "multiplication") operation. It suffices to describe this using a datatype with Return of 'a and Join of 'a t F.t, so the operations "stack" as we'd expect from a free gadget.

We then have the following signature:

signature FREE_MONAD = sig
  structure F : FUNCTOR;
  (* probably should rename the constructors to the more
  intuitive RETURN of 'a | JOIN of ('a t) F.t
  since $\mu$ corresponds to the `join` function for a monad.
  This `JOIN` constructor wraps the "outer" functor as a
  placeholder. *)
  datatype 'a t = Return of 'a
                | Join of ('a t) F.t;
  val return : 'a -> 'a t;
  val bind : 'a t -> ('a -> 'b t) -> 'b t;
  val join : 'a t t -> 'a t;
  val map : ('a -> 'b) -> 'a t -> 'b t;
  val lift : 'a F.t -> 'a t;
  (* lift is analogous to (fn x => [x]) *)
  (* fun lift x = Join (F.fmap Return x); *)

  (* val fold : ('a F.t -> 'a) -> 'a m -> 'a; *)
(* fun fold _ (Return a) = a
     | fold f (Join x) = f (F.fmap (fold f) x);
*)
end;

Note that we need to "hack" the SML module system to make this a functor. The type alias type 'a t = 'a m accomplishes this. See Bob Harper's Programming in SML, Section 18.1, for details. (We could have written something like include MONAD; include FUNCTOR where type 'a t = 'a m in the signature, but it would not change the implementation as a structure or functor).

Here Return and Join are [data] constructors for the free monad generated by the Functor F.

The bind function (which tells us everything we'd want to know about a monad) is the "default implementation" in terms of Join and F.map with some subtlety. Normally we would have x >>= f = join (F.map f x) but we need to "propagate" the (>>= f) down; i.e., we would have join (F.map (fn m => bind m f) x) be the bind function.

The bind implementation amounts to more of a map than anything else. (In fact, we need to patch this up later on if we want to use Free(F) as a monad; we can redefine fun bind m f = join (map f m) at the end of the functor structure's body to avoid this.)

Another way to approach this is to first implement the map function, then the join function, and then the bind function follows as the default implementation as bind m f = join (map f m) (see, e.g., Bartosz Milewski's Category Theory for Programmers, section 20.2).

Also observe we include the where type... clause to make public the underlying functor's type:

functor Free(F : FUNCTOR) :> FREE_MONAD
                               where type 'a F.t = 'a F.t
                                 = struct
  structure F = F;
  datatype 'a t = Return of 'a
                | Join of ('a t) F.t;
  (* return : 'a -> 'a t *)
  fun return x = Return x;

  fun map f (Return a) = Return (f a)
    | map f (Join x) = Join (F.map (map f) x);

  fun join (Return x) = x
    | join (Join x) = Join (F.map join x);

  fun bind m f = join (map f m);
  
  (* lift : 'a F.t -> 'a t *)
  fun lift f = Join (F.map return f);
end;

This is actually a bit more explicit than the Haskell type signatures, since Haskell does not distinguish which instance each fmap comes from.

We can use the free monad to describe a simple IO monad. Where to start?

First we need to construct a functor with the various operations we'd like to perform. For now, simply printing a string to the screen and reading a string from stdIn suffices.

We encode this as a datatype by making each operation with a signature like Foo : A -> B -> C -> Z IO.t corresponds to a data constructor FooOp of A * B * C * (Z -> 'a). This is the idiom for using free monads in functional programming: we have a functor describing the syntax tree for an embedded DSL, and we translate the type signature for each operation in the DSL into a type for the data constructor's payload as we have just sketched.

One caveat: if Z = unit (as would happen with print_line), then we can replace Z -> 'a with just 'a.

(* A functor describing the operations with side-effects in IO

In general, an operation `Foo : A -> B -> C -> Z IO.t` would
be encoded by a data constructor `FooOp of A * B * C * (Z -> 'a)`.

We also treat `unit -> 'a` as interchangeable with `'a`.
 *)
structure IO_Op = struct
  datatype 'a t = Print of (string * 'a)
                | Read of (string -> 'a);
  fun map f (Print (s,k)) = Print (s, f k)
    | map f (Read k) = Read (fn s => f (k s));
end;

We will also have a read_line function which we need to implement (it's straightforward):

fun read_line () =
  case TextIO.inputLine TextIO.stdIn of
      SOME s => s
    | NONE => "";

Now we can put all these pieces together to form the free monad describing IO side effects we prescribed:

local
  structure FreeIO = Free(IO_Op);
in
  structure Job : sig
      datatype t = datatype FreeIO.t
      val bind: 'a t -> ('a -> 'b t) -> 'b t
      val join: 'a t t -> 'a t
      val map: ('a -> 'b) -> 'a t -> 'b t
      val return: 'a -> 'a t
      val unsafePerform: 'a t -> 'a
  end = struct
    open FreeIO;
    (* datatype replication to make the constructors public *)
    datatype t = datatype FreeIO.t;
    (* execute the monad *)
    fun unsafePerform (Return x) = x
      | unsafePerform (Join f) =
        case f of
            (IO_Op.Print (s, k)) => (print s;
                                     unsafePerform k)
          | (IO_Op.Read k) => unsafePerform (k (read_line()));
  end
end;

We can now use the previous machinations in a toy example:

infix >> >>=
fun ((m : 'a Job.t) >>= (n : 'a -> 'b Job.t)) = Job.bind m n;
fun (m >> n) = Job.bind m (fn _ => n);

fun print_string msg =
  Job.Join (IO_Op.Print (msg, Job.Return ()));
val read_string =
  Job.Join (IO_Op.Read (fn msg => Job.Return msg));
fun main () =
  (print_string "What's your name? ") >>
    (read_string >>= (fn name => 
                       (print_string "Hello, ") >>
                         (print_string name)));

Job.unsafePerform (main ());

This isn't terribly different than the IO Monad implemented in Standard ML as found in Andrew Gordon's PhD dissertation.

• Nick Vanderweit's Free monads in OCaml