Free monad

The free monad on a functor $F$ is the monad whose values are trees of instructions of shape $F$ , with results at the leaves. It supplies the monad operations and satisfies the monad laws, and nothing else, so a program written in it is a description of what to do that can be interpreted afterwards: run for real, run against a test double, printed or analysed. Every way of interpreting the instructions in some monad extends in exactly one way to an interpreter for whole programs^[6]. Free monads are a standard way to build embedded languages in Haskell^[1], and are closely related to algebraic effects and effect handlers^[4].

§ 01

Definition

Given a functor $F$ , the free monad $Free F$ is the recursive type

Free F a = Pure a ∣ Free (F (Free F a))

A value is either finished, with a result, or an instruction of shape $F$ whose positions hold the rest of the computation. The monad operations substitute at the leaves:

return x = Pure x Pure x > > = f = f x Free fx > > = f = Free (fmap (λm . m > > = f) fx)

Bind walks down the tree and grafts $f$ onto every leaf; it uses nothing about $F$ except $fmap$ . A single instruction is lifted into the monad by putting $Pure$ in its positions, $lift fx = Free (fmap Pure fx)$ . The monad laws hold because bind is substitution in a tree.

With $F x = x$ , a value of the free monad is a result together with a number of steps taken to reach it; with $F x = 1$ , the one-element type, it is the option monad; with $F x = A \times x$ it is the writer monad over lists of $A$ .

§ 02

Programs as data

An instruction set is a functor whose constructors are the operations. An operation that returns an answer holds the rest of the program as a function of the answer; one that returns nothing holds the rest directly. A program built with bind is then a data structure, and running it is a separate function, an interpreter:

A key-value store as a free monad: instructions, a program, and two interpreters.

module type FUNCTOR = sig
  type 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end
 
(* The free monad on a functor F: a tree of F-shaped nodes with values at
   the leaves. *)
module Free (F : FUNCTOR) = struct
  type 'a t = Pure of 'a | Free of 'a t F.t
 
  let return x = Pure x
  let rec bind m f = match m with Pure x -> f x | Free fx -> Free (F.map (fun m -> bind m f) fx)
  let ( let* ) = bind
  let lift fx = Free (F.map return fx)
end
 
(* The instructions of a key-value store. Each carries the rest of the
   program, as a value or as a function of the instruction's answer. *)
module Cmd = struct
  type 'k t = Get of string * (string option -> 'k) | Put of string * string * 'k
  let map f = function Get (k, next) -> Get (k, fun v -> f (next v)) | Put (k, v, next) -> Put (k, v, f next)
end
 
module KV = Free (Cmd)
open KV
 
let get k = lift (Cmd.Get (k, Fun.id))
let put k v = lift (Cmd.Put (k, v, ()))
 
(* A program: data only, nothing has run yet. *)
let visit user =
  let* n = get ("visits:" ^ user) in
  let n = match n with Some s -> int_of_string s + 1 | None -> 1 in
  let* () = put ("visits:" ^ user) (string_of_int n) in
  let* () = if n = 1 then put ("first:" ^ user) "yes" else return () in
  return n
 
(* Interpreter 1: run against an in-memory map. *)
module SMap = Map.Make (String)
let rec run_map store = function
  | Pure x -> (x, store)
  | Free (Cmd.Get (k, next)) -> run_map store (next (SMap.find_opt k store))
  | Free (Cmd.Put (k, v, next)) -> run_map (SMap.add k v store) next
 
(* Interpreter 2: print the commands, answering every get with a fixed value. *)
let rec describe answer = function
  | Pure _ -> []
  | Free (Cmd.Get (k, next)) -> ("GET " ^ k) :: describe answer (next answer)
  | Free (Cmd.Put (k, v, next)) -> ("PUT " ^ k ^ " " ^ v) :: describe answer next

Running it.

run_map:   result [1; 2; 1]
           first:ada = yes
           first:bob = yes
           visits:ada = 2
           visits:bob = 1
describe (every get answered None):
           GET visits:ada
           PUT visits:ada 1
           PUT first:ada yes
describe (every get answered Some "41"):
           GET visits:ada
           PUT visits:ada 42

The same visit program is run against a map and described as a list of commands. The description shows that the program's behaviour depends on the answers it receives: when the key is missing, it records a first visit. An interpreter could equally send the commands to a database, log them, check them against a permission policy, or replay recorded answers in a test. Swierstra and Altenkirch used this to give a pure semantics to input and output, mutable references and concurrency, so that programs using them can be tested^[8].

§ 03

Universal property

An interpreter for a single instruction is a natural transformation $φ : F \Rightarrow M$ into some monad $M$ . The free monad's defining property is that each such $φ$ extends uniquely to a monad morphism $φ^: Free F \Rightarrow M$ that agrees with it on single instructions^[6]:

φ^(Pure x) = return_{M} x φ^(Free fx) = φ (fx) > > =_{M} φ^

In Haskell this function is called foldFree. Being a monad morphism, it respects $return$ and $> > =$ , so interpreting a program built from two parts is the same as interpreting the parts and combining them in $M$ . In categorical terms, $Free$ is left adjoint to the functor that forgets the monad structure of a monad, and the free monad on $F$ exists when $F$ is sufficiently well behaved, for example when it is a polynomial functor^[6]. The analogy is with the free monoid: lists are sequences of elements with concatenation and nothing else, and a free monad is a sequence of instructions with sequencing and nothing else.

Algebraic effects

Plotkin and Power observed that the monads for many computational effects are free monads on the effect's operations, quotiented by equations between them, such as "writing a location and then reading it returns what was written"^[5]. Plotkin and Pretnar's handlers of algebraic effects are the interpreters of such free monads, written as a construct of the language^[4], and OCaml 5's effect handlers implement the same idea with continuations captured on the stack instead of a data structure^[9].

§ 04

Performance

Bind traverses the tree to its leaves, so a program built with binds nested to the left, $((m > > = f_{1}) > > = f_{2}) > > = \dots$ , traverses the growing tree once for every bind and takes time quadratic in its length. It is the same problem as appending to the end of a list repeatedly. The Church-encoded form, also called the codensity transformation, represents a computation as a function of what to do with its result, which reassociates every bind to the right^[3]:

Church F a = \forall r . (a \to Free F r) \to Free F r

Left-nested binds on the free monad and on its Church encoding, counting calls to fmap.

(* Left-nested binds on the free monad are quadratic: each bind walks
   down the whole tree built so far. The Church-encoded (codensity) form
   reassociates them and is linear. *)
module Tick = struct
  type 'k t = Tick of 'k
  let maps = ref 0
  let map f (Tick k) = incr maps; Tick (f k)
end
 
type 'a free = Pure of 'a | Free of 'a free Tick.t
 
let rec bind m f = match m with Pure x -> f x | Free fx -> Free (Tick.map (fun m -> bind m f) fx)
let tick = Free (Tick.Tick (Pure ()))
 
(* ((tick >>= fun () -> tick) >>= fun () -> tick) >>= ... n times *)
let left_nested n = let rec go m i = if i = 0 then m else go (bind m (fun () -> tick)) (i - 1) in go (Pure ()) n
 
let rec length = function Pure _ -> 0 | Free (Tick.Tick k) -> 1 + length k
 
(* Church form: a computation is a function of what to do with its result. *)
type 'a church = { run : 'r. ('a -> 'r free) -> 'r free }
 
let c_return x = { run = (fun k -> k x) }
let c_bind m f = { run = (fun k -> m.run (fun x -> (f x).run k)) }
let c_tick = { run = (fun k -> Free (Tick.map k (Tick.Tick ()))) }
let c_left_nested n = let rec go m i = if i = 0 then m else go (c_bind m (fun () -> c_tick)) (i - 1) in go (c_return ()) n
let to_free m = m.run (fun x -> Pure x)

Running it.

     n     free: maps   church: maps
  1000         499500           1000
  2000        1999000           2000
  4000        7998000           4000
  8000       31996000           8000

The plain version makes $n (n - 1) /2$ calls to fmap and the Church-encoded one $n$ . The Church form cannot be inspected without being run, so libraries convert between the two. Van der Ploeg and Kiselyov gave a representation that keeps the tree inspectable and makes both building and inspecting efficient, by storing the continuations in a type-aligned sequence^[7].

§ 05

Variants

The freer monad, or operational monad, drops the requirement that the instructions form a functor: an instruction is a GADT constructor whose type index is its answer type, and the continuation is stored separately^[2]:

Freer I a = Pure a ∣ \exists x . Impure (I x) (x \to Freer I a)

This removes the boilerplate of writing fmap for every instruction set. Swierstra's "data types à la carte" combines instruction sets as sums of functors, so that a program can use operations from several sets and an interpreter can handle one set and pass the rest on^[1], which is the basis of extensible-effects libraries^[2]. The free applicative, built analogously for applicative functors, gives programs whose sequence of instructions is fixed in advance and can be inspected before any of them runs.

§ 06

History

Free monads are a construction of category theory, as the monads arising from free algebras^[6]. In functional programming they became known as a way of building interpreters in the 2000s: Swierstra and Altenkirch used them to model effects in 2007^[8], Swierstra's "data types à la carte" in 2008 showed how to combine them^[1], and Voigtländer in the same year showed how to remove the quadratic cost of left-nested binds^[3]. Kiselyov and Ishii's freer monads of 2015 simplified the definition^[2].