A Helping Phantom Hand

You don't have to be writing an interpreter or some other kind of abstract code to profit from some phantom types. Suppose you have two or more functions that work by "cooking" a simple value (a float, say) with a lengthy computation before proceeding:

let sun_geometric_longitude j =
  let je = to_jcen (to_jde j) in
  (* … computation with je … *)

let sun_apparent_longitude j =
  let je = to_jcen (to_jde j) in
  let q  = sun_geometric_longitude j in
  (* … computation with je … *)

In this case j is a date expressed in Julian Days as a float, and to_jde computes the Ephemeris Time as a 63-term trigonometric polynomial correction on it. sun_apparent_longitude calls sun_geometric_longitude and both call to_jde. Obviously this unnecessary duplication can be factored out:

let sun_geometric_longitude je =
  let t  = to_jcen je in
  (* … computation with je … *)

let sun_apparent_longitude je =
  let q  = sun_geometric_longitude je in
  let t  = to_jcen je in
  (* … computation with je … *)

let foo j =
  let je = to_jde j in
  let l  = sun_apparent_longitude je in
  (* … *)

(to_jcen is cheap and not worth factoring out.) But now a naked float represent two different things, Universal Time and Ephemeris Time, and we have a valid concern of mixing them up. We can wrap the time in an ADT:

type dt = UT of float | TD of float

let to_jcen j = match j with
| UT j ->
  (* … lengthy computation … *)
  TD j
| TD _ -> invalid_arg "to_jcen"

let sun_geometric_longitude je = match je with
| TD je ->
  let t  = to_jcen je in
  (* … computation with je … *)
| UT _  -> invalid_arg "sun_geometric_longitude"

let sun_apparent_longitude je = match je with
| TD je ->
  let q  = sun_geometric_longitude je in
  let t  = to_jcen je in
  (* … computation with je … *)
| UT _  -> invalid_arg "sun_apparent_longitude"

let foo j =
  let je = to_jde j in
  (* … computation with sun_apparent_longitude je … *)

but this forces us to check at run-time whether we mixed times up in our code. A better technique is to use a phantom type. First fix an abstract signature for the module implementing these functions:

module Test : sig
  type 'a dt

  val datetime : yy:int -> mm:int -> dd:int -> hh:int -> nn:int -> ss:float -> [ `JD ] dt
  val to_jde   : [ `JD ] dt -> [ `JDE ] dt
  val to_jcen  : 'a dt -> float

  val sun_geometric_longitude : [ `JDE ] dt -> float
  val sun_apparent_longitude  : [` JDE ] dt -> float
end = struct
  (* … *)

We have a way to construct our type α dt from a Universal datetime, a way to convert it to Dynamical Time with to_jde and operations that respect the kind of measure. The implementation is as before:

  (* … *)
  type 'a dt = float (* phantom type! *)

  let datetime ~yy ~mm ~dd ~hh ~nn ~ss = (* … *)

  let to_jde  j = (* … *)
  let to_jcen j = (* … *)

  let sun_geometric_longitude je =
    (* … computation with a statically checked je … *)

  let sun_apparent_longitude je =
    let q  = sun_geometric_longitude je in
    (* … computation with a statically checked je … *)
end

Now the compiler checks for us that we don't mix up measures. The only inconvenient of this approach is that the type α dt is fully abstract, and you must provide coercions, string_ofs and pretty printers for it if you need to show them or debug your code. There is a way out, though; just make it a private type abbreviation:

module Test : sig
  type 'a dt = private float
  (* … signature exactly as before … *)
end = struct
  type 'a dt = float (* phantom type! *)
  (* … implementation exactly as before … *)
end

Now α dt will be shown in the top-level, can be printed with a coercion (je :> float), etc.

For another simple example, suppose you want to represent sets as lists. The best way to do that is to keep them sorted so that set operations run in linear time. If you want to provide some operations that temporarily destroy the ordering, a phantom type can keep track of the invariant "this list is sorted":

module Set : sig
  type ('a, 'b) t = private 'a list

  val of_list : 'a list -> ('a, [ `S ]) t
  val as_set  : ('a, [ `U ]) t -> ('a, [ `S ]) t
  val empty   : ('a, [ `S ]) t
  val mem     : 'a -> ('a, [ `S ]) t -> bool
  val add     : 'a -> ('a, [ `S ]) t -> ('a, [ `S ]) t
  val union   : ('a, [ `S ]) t -> ('a, [ `S ]) t -> ('a, [ `S ]) t
  val inter   : ('a, [ `S ]) t -> ('a, [ `S ]) t -> ('a, [ `S ]) t
  val append  : ('a, 'b) t -> ('a, 'c) t -> ('a, [ `U ]) t
end = struct
  type ('a, 'b) t = 'a list

  let of_list l   = List.sort compare l
  and as_set  l   = List.sort compare l
  and empty       = []
  let union   l r = (* … linear merge … *)
  and inter   l r = (* … linear merge … *)
  let mem     e   = List.mem e
  and add     e   = union [e]
  and append      = List.append
end

The phantom type [ `S | `U ] tracks the sortedness of the list. Note that in the case of append the argument lists can have any ordering but the result is known to be unsorted. Note also how the fact that the empty list is by definition sorted is directly reflected in the type.

Theorems for Free: The Monad Edition

This is for the record, since the derivations took me a while and I'd rather not lose them.

A functor is the signature:

module type FUNCTOR = sig
  type 'a t
  val fmap : ('a -> 'b) -> ('a t -> 'b t)
end

satisfying the following laws:

Identity:    fmap id      ≡ id
Composition: fmap (f ∘ g) ≡ fmap f ∘ fmap g

An applicative structure or idiom is the signature:

module type APPLICATIVE = sig
  type 'a t
  val pure : 'a -> 'a t
  val ap : ('a -> 'b) t -> ('a t -> 'b t)
end

satisfying the following laws:

Identity:     ap (pure id)                  ≡ id
Composition:  ap (ap (ap (pure (∘)) u) v) w ≡ ap u (ap v w)
Homomorphism: ap (pure f) ∘ pure            ≡ pure ∘ f
Interchange:  ap u (pure x)                 ≡ ap (pure (λf.f x)) u

An applicative functor is the structure:

module type APPLICATIVE_FUNCTOR = sig
  type 'a t
  include FUNCTOR     with type 'a t := 'a t
  include APPLICATIVE with type 'a t := 'a t
end

that is simultaneously a functor and an applicative structure, satisfying the additional law:

Fmap: fmap ≡ ap ∘ pure

A monad is the structure:

module type MONAD = sig
  type 'a t
  val return : 'a -> 'a t
  val bind : ('a -> 'b t) -> ('a t -> 'b t)
end

satisfying the following laws:

Right unit:    bind return     ≡ id
Left unit:     bind f ∘ return ≡ f
Associativity: bind f ∘ bind g ≡ bind (bind f ∘ g)

Every monad is an applicative functor:

module ApplicativeFunctor (M : MONAD)
: APPLICATIVE_FUNCTOR with type 'a t = 'a M.t
= struct
  type 'a t = 'a M.t
  open M
  let fmap f = bind (fun x -> return (f x))
  let pure   = return
  let ap u v = bind (fun f -> fmap f v) u
end

This can be proved by easy (but tedious) equational reasoning. That the proof is rigorous is Wadler's celebrated result.

Proof of the Functor Identity:

  fmap id
≡ { definition }
  bind (return ∘ id)
≡ { composition }
  bind return
≡ { Monad Right unit }
  id

Proof of the Functor Composition:

  fmap f ∘ fmap g
≡ { definition }
  bind (return ∘ f) ∘ bind (return ∘ g)
≡ { Monad Associativity }
  bind (bind (return ∘ f) ∘ return ∘ g)
≡ { Monad Left unit }
  bind (return ∘ f ∘ g)
≡ { definition }
  fmap (f ∘ g)

A number of naturality conditions are simple equations between λ-terms. I'll need these later:

Lemma 1 (Yoneda):

  fmap f ∘ (λh. fmap h x)
≡ { defn. ∘, β-reduction }
  λg. fmap f (fmap g x)
≡ { defn. ∘ }
  λg. (fmap f ∘ fmap g) x
≡ { Functor Composition }
  λg. fmap (f ∘ g) x
≡ { abstract }
  λg. (λh. fmap h x) (f ∘ g)
≡ { defn. ∘, η-contraction }
  (λh. fmap h x) ∘ (f ∘)

Lemma 2:

  fmap f ∘ return
≡ { definition }
  bind (return ∘ f) ∘ return
≡ { Monad Left unit }
  return ∘ f

Lemma 3:

  bind f ∘ fmap g
≡ { definition fmap }
  bind f ∘ bind (return ∘ g)
≡ { Monad Associativity }
  bind (bind f ∘ return ∘ g)
≡ { Monad Left unit }
  bind (f ∘ g)

Lemma 4:

  bind (fmap f ∘ g)
≡ { definition fmap }
  bind (bind (return ∘ f) ∘ g)
≡ { Monad Associativity }
  bind (return ∘ f) ∘ bind g
≡ { definition fmap }
  fmap f ∘ bind g

The Applicative Functor condition is easy to prove and comes in as a handy lemma:

  ap ∘ pure
≡ { definition }
  λv. bind (λf. fmap f v) ∘ return
≡ { Monad Left unit }
  λv. λf. fmap f v
≡ { η-contraction }
  fmap

Proof of the Applicative Identity:

  ap (pure id)
≡ { Applicative Functor }
  fmap id
≡ { Functor Identity }
  id

Proof of the Applicative Homomorphism:

  ap (pure f) ∘ pure
≡ { Applicative Functor }
  fmap f ∘ pure
≡ { Lemma 2, defn. pure }
  pure ∘ f

Proof of the Applicative Interchange:

  ap (pure (λf.f x)) u
≡ { Applicative Functor }
  fmap (λf.f x) u
≡ { definition }
  bind (return ∘ (λf.f x)) u
≡ { defn. ∘, β-reduction }
  bind (λf. return (f x)) u
≡ { Lemma 2 }
  bind (λf. fmap f (return x)) u
≡ { definition }
  ap u (pure x)

The proof of the Applicative Composition condition is the least straightforward of the lot, as it requires ingenuity to choose the reduction to apply at each step. I started with a long, tedious derivation that required forward and backward reasoning; at the end I refactored it in byte-sized lemmas in order to simplify it as much as I could. As a heuristic, I always try to start from the most complicated expression to avoid having to guess where and what to abstract (that is, applying elimination rules requires neatness, while applying introduction rules requires backtracking):

  ap (ap (ap (pure (∘)) u) v) w
≡ { Applicative Functor }
  ap (ap (fmap (∘) u) v) w
≡ { definition }
  bind (λf. fmap f w) (bind (λf. fmap f v) (fmap (∘) u))
≡ { Lemma 3 with f := λf. fmap f v, g := (∘) }
  bind (λf. fmap f w) (bind ((λf. fmap f v) ∘ (∘)) u)
≡ { Monad Associativity with f := λf. fmap f w, g := (λf. fmap f v) ∘ (∘) }
  bind (bind (λf. fmap f w) ∘ (λf. fmap f v) ∘ (∘)) u
≡ { defn. ∘ (at right) }
  bind (λf. (bind (λf. fmap f w) ∘ (λf. fmap f v)) (f ∘)) u
≡ { defn. ∘, β-reduction }
  bind (λf. bind (λf. fmap f w) (fmap (f ∘) v)) u
≡ { Lemma 3 with f := λf. fmap f w, g := (f ∘) }
  bind (λf. bind ((λf. fmap f w) ∘ (f ∘)) v) u
≡ { Lemma 1 }
  bind (λf. bind (fmap f ∘ (λf. fmap f w)) v) u
≡ { Lemma 4 with g := λf. fmap f w }
  bind (λf. fmap f (bind (λf. fmap f w) v)) u
≡ { definition }
  ap u (ap v w)

What is this good for? I don't really know; Haskellers can't seem to be able to live without them while I can't seem to justify their application. I suspect laziness has a lot to do with it; in any case, the machinery is more palatable with the appropriate combinators:

module Functor (F : FUNCTOR) = struct
  include F
  let ( <$> ) = fmap
end

module Applicative (A : APPLICATIVE) = struct
  include A
  let ( <*> ) = ap
end

module Monad (M : MONAD) = struct
  include M
  include (ApplicativeFunctor (M)
         : APPLICATIVE_FUNCTOR with type 'a t := 'a t)
  let ( <$> )     = fmap
  let ( <*> )     = ap
  let ( >>= ) m f = bind f m
end

An Odd Lemma

While proving that every monad is an applicative functor, I extracted the following derivation as a lemma:

  fmap f ∘ (λh. fmap h x)
≡ { defn. ∘, β-reduction }
  λg. fmap f (fmap g x)
≡ { defn. ∘ }
  λg. (fmap f ∘ fmap g) x
≡ { Functor }
  λg. fmap (f ∘ g) x
≡ { abstract f ∘ g }
  λg. (λh. fmap h x) (f ∘ g)
≡ { defn. ∘, η-contraction }
  (λh. fmap h x) ∘ (f ∘)

for all f, x. This is the Yoneda Lemma in a special form. The term λh. fmap h x is the natural transformation between an arbitrary functor F and the functor Hom(X, —), where X is fixed by the type of x. Dan Piponi calls it the hardest trivial thing in mathematics. I didn't recognize it immediately (my category-fu is nonexistent), but the striking symmetry made me curious and I started investigating.

Existential Crisis

In a long discussion at LtU, user Jules Jacobs advances a use-case that for him would have been difficult to solve in a statically-typed language. I focus on his first two points:

1. A data structure that is a container of T plus a function on T's. I would have needed existential types to hide the T, which I don't get in many languages.
2. A couple of functions that take heterogeneous list of items that the function will convert to the interface it needs the elements to be with an extensible conversion function. […]

It's true, not many languages have existential types but OCaml happens to do, or at least allows existentials to be encoded. I'll take a big hint from MLton and I'll try to solve both problems (I won't pretend to solve his actual problems; just my interpretation of the problems he posed). Another reason why I write this post is because I always forget what the essence of existential types is. Pierce writes:

Similarly, there are two different ways of looking at an existential type, written {∃X,T}. The logical intuition is that an element of {∃X,T} is a value of type [X ↦ S]T, for some type S. The operational intuition, on the other hand, is that an element of {∃X,T} is a pair, written {*S,t}, of a type S and a term t of type [X ↦ S]T.

[…] To understand existential types, we need to know two things: how to build (or introduce, in the jargon of §9.4) elements that inhabit them, and how to use (or eliminate) these values in computations.

An existentially typed value is introduced by pairing a type with a term, written {*S,t}. A useful concrete intuition is to think of a value {*S,t} of type {∃X,T} as a simple form of package or module with one (hidden) type component and one term component. The type S is often called the hidden representation type, or sometimes (to emphasize a connection with logic, cf. §9.4) the witness type of the package. For example, the package p = {*Nat, {a=5, f=λx:Nat. succ(x)}} has the existential type {∃X, {a:X, f:X→X}}. The type component of p is Nat, and the value component is a record containing a field a of type X and a field f of type X→X, for some X (namely Nat).

(Types and Programming Languages, p. 363–364) I quote at some length because Pierce's presentation is so condensed that for me it really bears repeating; also, because every time I want a refresher I can come to this post instead of cracking open the physical book. The gist of it is pithily and more memorably stated in Mitchell and Plotkin's slogan, abstract types have existential type.

The complication is that in ML types are not values, so in order to pack an existential we must reify the type component as a term, for instance as a pair of functions, an injection and a projection:

module type UNIV = sig
  type t
  val embed : unit -> ('a -> t) * (t -> 'a)
end

Why UNIV when we're talking about existential types? Go ask Oleg. Actually, there is a type isomorphism analogous to the logical equivalence between (∃x. P x) ⇒ Q and ∀x.(P x ⇒ Q); as Jeremy Gibbons writes …the justification being that a datatype declaration such as type e = ∃t. E of t foo introduces a constructor E : (∃t. t foo) → e, and this type is isomorphic to ∀t.(t foo → e) because e is independent of t… (Haskellisms paraphrased).

In any case, here the existential type is t, and embed produces a (inj, prj) pair that can be applied to values of some type α. Only the prj of the pair can recover the injected value; the use of any other prj will fail. There are at least two possible implementations, one using references and another one using exceptions (which are values of a single open, extensible, generative type). The latter is very clever:

module Univ : UNIV = struct
  type t = exn
  let embed (type u) () =
    let module E = struct
      exception E of u
      let inj x = E x
      let prj = function E x -> x | _ -> raise Not_found
    end in E.(inj, prj)
end

The use of the named type u and a local module are 3.12 features that allow declaring a polymorphic exception (compare the SML solution in MLton's website). Since the exception constructor E is different for every invocation of embed (this is the "generative" bit referred to above), only the prj of the pair can recover the value:

let () =
  let inj_int  , prj_int   = Univ.embed ()
  and inj_float, prj_float = Univ.embed () in
  let r = ref (inj_int 13) in
  let s1 = try string_of_int   (prj_int   !r) with Not_found -> "None" in
  r := inj_float 13.0;
  let s2 = try string_of_int   (prj_int   !r) with Not_found -> "None" in
  let s3 = try string_of_float (prj_float !r) with Not_found -> "None" in
  Printf.printf "%s %s %s\n" s1 s2 s3

Note that the reference r holds values "of different types" via the corresponding inj. This code typechecks and when run outputs:

13 None 13.

On top of this "universal" existential type we can build heterogeneous property lists à la Lisp (see again MLton's site):

module PList : sig
  type t
  val make     : unit -> t
  val property : unit -> (t -> 'a -> unit) * (t -> 'a)
end = struct
  type t = Univ.t list ref

  let make () = ref []

  let property (type u) () =
    let inj, prj = Univ.embed () in
    let put r v = r := inj v :: !r
    and get r   =
      let rec go = function
      | []      -> raise Not_found
      | x :: xs -> try prj x with Not_found -> go xs
      in go !r
    in (put, get)
end

Each property must be created explicitly but independently of any list using it. They encapsulate an existentially-typed value; look-up just proceeds by attempting to project out the corresponding value. These lists really are magical:

let () =
  let put_name  , get_name   = PList.property ()
  and put_age   , get_age    = PList.property ()
  and put_weight, get_weight = PList.property () in
  let show p = Printf.printf "%s: %d years, %.1f kg\n"
    (get_name   p)
    (get_age    p)
    (get_weight p)
  in
  let boy, girl = PList.make (), PList.make () in
  put_name   boy  "Tim";
  put_age    boy  13;
  put_weight boy  44.0;
  put_name   girl "Una";
  put_age    girl 12;
  put_weight girl 39.0;
  List.iter show [boy; girl]

Here boy and girl are two different, independent property lists that act as extensible records with labels get_name, get_age and get_weight. The list iteration prints the properties uniformly via show, without having to cast or do any strange contortions (at least not any outside the definitions). The output is:

Tim: 13 years, 44.0 kg
Una: 12 years, 39.0 kg

Of course nothing says that the property lists must be homogeneous in the properties they contain; looking for an inexistent property will simply fail. On the other hand, probably the preferred way to handle extensible records in OCaml is via objects, using structural subtyping in the same way dynamically-typed languages would use duck typing. This would make solving the original problem a little more familiar to Python or Ruby programmers; but then, recovering the original objects from the lists would be impossible without downcasts.

Brainfuck in Java

(I don't feel like writing a punning title.) Last time I showed how the use of functors allows for modular and type-safe specification of semantics. I wrote I can't imagine this flexibility in object-oriented languages like Java or Python; fighting words for which I was justly taken to task. Here's my penance: a morally equivalent reimplementation in Java of the Brainfuck interpreter. The translation was mechanic, but I realized with some surprise that the result is more flexible than the original OCaml: whereas the latter only allows static composition of semantics (unless you use first-class modules), Java allows fully dynamic, run-time stacking of semantics.

Even though the Java is better decoupled than the original (which uses the same memory representation for every interpreter variant), this is more by necessity than design. In the process, the interpreter suffered more than a 300% code expansion by line count at 520 lines. Bear with me! This is a single-file, multiple-class program; feel free to package and refactor it to your heart's content. The external requirements are minimal:

import java.io.IOException;
import java.util.ArrayList;
import java.util.List;
import java.util.Stack;

As advertised, the top-level Brainfuck class parses, prints and evaluates Brainfuck programs (a List of Instructions) using fully compositional semantics:

public final class Brainfuck {
    public static void main(String[] args) {
        String hello =
">+++++++++[<++++++++>-]<.>+++++++[<++++>-]<+.+++++++..+++.>>>++++++++[<++++>-]"+
"<.>>>++++++++++[<+++++++++>-]<---.<<<<.+++.------.--------.>>+.";
        Semantics semantics = new S3_(5000, new S2(new S1_(new S0())));
        List<Instruction> program = Brainfuck.parse(hello);
        System.out.print(Brainfuck.print(program));
        Brainfuck.evaluate(semantics, program);
    }

The class is completely static and reentrant; the main operations delegate to appropriate visitors:

private Brainfuck() { }

    public static void evaluate(Semantics semantics, List<Instruction> program) {
        new Evaluator(semantics).evaluate(program);
    }

    public static String print(List<Instruction> program) {
        return new Printer().print(program);
    }

The parser is standard, recursive-descent but with explicitly-managed recursion. For simple (concrete) instructions it just adds the corresponding Instruction to the current program. When it sees an opening bracket it uses a Stack to hold the partially-parsed List of Instructions and starts fresh. When it encounters a closing bracket, it builds a Repeat instruction from the just-parsed program, pops the context and adds the former to the latter:

public static List<Instruction> parse(String text) {
        final Stack<List<Instruction> > stack = new Stack<List<Instruction> >();
        List<Instruction> program = new ArrayList<Instruction>();

        for (int i = 0; i != text.length(); i++)
            switch (text.charAt(i)) {
            case '>': program.add(Instruction.FWD); break;
            case '<': program.add(Instruction.BAK); break;
            case '+': program.add(Instruction.INC); break;
            case '-': program.add(Instruction.DEC); break;
            case '.': program.add(Instruction.OUT); break;
            case ',': program.add(Instruction.INP); break;
            case '[':
                stack.push(program);
                program = new ArrayList<Instruction>();
                break;
            case ']':
                if (stack.empty())
                    throw new IllegalArgumentException("unmatched `]'");
                final Instruction rep = Instruction.REP(program);
                program = stack.pop();
                program.add(rep);
                break;
            }
        if (!stack.empty())
            throw new IllegalArgumentException("unmatched `['");
        return program;
    }
}

A textbook example that completes the class. Now for the real program. An Instruction is an abstract class implementing the case class pattern à la Scala (cf Wadler's expression problem). Every instruction supports two operations, evaluation and printing, by using the visitor pattern:

abstract class Instruction {
    private Instruction() { }

    public abstract void evaluate(Evaluator evaluator);
    public abstract void print(Printer printer);

Each concrete Instruction is tucked away inside this class. They simply forward the call to the passed-in visitor. The first six are mind-numbingly straightforward:

private static final class Forward extends Instruction {
        private Forward() { }

        @Override
        public void evaluate(Evaluator evaluator) {
            evaluator.evaluateForward();
        }

        @Override
        public void print(Printer printer) {
            printer.printForward();
        }

    private static final class Backward extends Instruction {
        private Backward() { }

        @Override
        public void evaluate(Evaluator evaluator) {
            evaluator.evaluateBackward();
        }

        @Override
        public void print(Printer printer) {
            printer.printBackward();
        }

    private static final class Increment extends Instruction {
        private Increment() { }

        @Override
        public void evaluate(Evaluator evaluator) {
            evaluator.evaluateIncrement();
        }

        @Override
        public void print(Printer printer) {
            printer.printIncrement();
        }

    private static final class Decrement extends Instruction {
        private Decrement() { }

        @Override
        public void evaluate(Evaluator evaluator) {
            evaluator.evaluateDecrement();
        }

        @Override
        public void print(Printer printer) {
            printer.printDecrement();
        }

    private static final class Output extends Instruction {
        private Output() { }

        @Override
        public void evaluate(Evaluator evaluator) {
            evaluator.evaluateOutput();
        }

        @Override
        public void print(Printer printer) {
            printer.printOutput();
        }

    private static final class Input extends Instruction {
        private Input() { }

        @Override
        public void evaluate(Evaluator evaluator) {
            evaluator.evaluateInput();
        }

        @Override
        public void print(Printer printer) {
            printer.printInput();
        }

The last Instruction is fractionally more interesting in that it has a program as a parameter:

private static final class Repeat extends Instruction {
        private final List<Instruction> program;

        private Repeat(List<Instruction> program) {
            this.program = program;
        }

        @Override
        public void evaluate(Evaluator evaluator) {
            evaluator.evaluateRepeat(program);
        }

        @Override
        public void print(Printer printer) {
            printer.printRepeat(program);
        }

These classes are fully private to the enclosing case class Instruction; the Brainfuck interpreter uses static members to refer to each:

public static final Instruction FWD = new Forward();
    public static final Instruction BAK = new Backward();
    public static final Instruction INC = new Increment();
    public static final Instruction DEC = new Decrement();
    public static final Instruction OUT = new Output();
    public static final Instruction INP = new Input();

    public static Instruction REP(List<Instruction> program) {
        return new Repeat(program);
    }
}

This is all the (essentially boilerplate) code necessary just to reproduce an algebraic data type over which OCaml code would pattern match. The visitors implement each arm of this match, so more boilerplate follows. The first one is the Evaluator:

class Evaluator {
    private final Semantics semantics;
    private final Memory memory;

It takes a Semantics and sets itself to operate upon an initial Memory:

public Evaluator(Semantics semantics) {
        this.semantics = semantics;
        this.memory = semantics.initial();
    }

This is all a bit abstract because both Semantics and Memory are interfaces that can be plugged-in at will. To evaluate a program, it visits each Instruction in turn:

public void evaluate(List<Instruction> program) {
        for (Instruction instruction : program)
            instruction.evaluate(this);
    }

Again, this is a bog-standard visitor. Each visiting method simply delegates to the chosen Semantics with the current state of the Memory:

public void evaluateForward() {
        semantics.forward(this.memory);
    }

    public void evaluateBackward() {
        semantics.backward(this.memory);
    }

    public void evaluateIncrement() {
        semantics.increment(this.memory);
    }

    public void evaluateDecrement() {
        semantics.decrement(this.memory);
    }

    public void evaluateOutput() {
        semantics.output(this.memory);
    }

    public void evaluateInput() {
        semantics.input(this.memory);
    }

The Repeat instruction is an Action over a Memory that corresponds to evaluate-ing the repeated program:

public void evaluateRepeat(final List<Instruction> program) {
        semantics.repeat(new Action<Memory>() {
            @Override
            public void apply(Memory _unused) {
                evaluate(program);
            }
        }, this.memory);
    }
}

(Why is the Memory _unused? Because evaluate already has it in scope, but the Semantics are fully parametric with respect to the store. If you find an elegant solution to this that doesn't involve each Instruction passing the Memory around, let me know.) This is the moral equivalent of a higher-order closure; someday you might be able to write a lambda instead of that. The second visitor is the Printer:

class Printer {
    private final StringBuffer buffer = new StringBuffer(72);
    private int linelen;

It formats the Brainfuck program in neat lines of 72 characters:

public Printer() {
        linelen = 0;
    }

    private void putc(char c)  {
        if (linelen == 72 || c == '\n') {
            buffer.append('\n');
            linelen = 0;
        }
        if (c != '\n') {
            buffer.append(c);
            linelen++;
        }
    }

The visitor sets the buffer up, prints each instruction by visiting them in turn and closes the buffer:

public String print(List<Instruction> program) {
        buffer.setLength(0);
        for (Instruction instruction : program)
            instruction.print(this);
        putc('\n');
        return buffer.toString();
    }

Each visited Instruction accumulates its representation in the buffer:

public void printForward()   { putc('>'); }
    public void printBackward()  { putc('<'); }
    public void printIncrement() { putc('+'); }
    public void printDecrement() { putc('-'); }
    public void printOutput()    { putc('.'); }
    public void printInput()     { putc(','); }

Aside: It is not the responsibility of the Instruction to know its external representation since it denotes Brainfuck's abstract syntax. Do not be misled by phony invocations to the Law of Demeter.

Repeat just emits its list of Instructions between brackets by mutual recursion between it and this visitor:

public void printRepeat(List<Instruction> program) {
        putc('[');
        for (Instruction instruction : program)
            instruction.print(this);
        putc(']');
    }
}

Neat. Now for the raison d'être of the exercise: A Semantics encapsulates the effects of each Brainfuck instruction upon the Memory:

interface Semantics {
    Memory initial();
    void forward(Memory memory);
    void backward(Memory memory);
    void increment(Memory memory);
    void decrement(Memory memory);
    void output(Memory memory);
    void input(Memory memory);
    void repeat(Action<Memory> program, Memory memory);
}

The effect of a repetition depends on the program being repeated; this is represented by an Action taking the Memory as a parameter:

interface Action<T> {
    void apply(T argument);
}

Aside: Don't confuse a program as a List of Instructions with its meaning as an Action or effect. It wouldn't be appropriate for repeat to take anything else.

In object-oriented languages there are two reuse mechanisms: inheritance and composition. The first is static, compile-time and determined by the providing (i.e. library) code; the second is dynamic, run-time and controlled by the consuming (i.e. client) code. Coplien's envelope pattern allows to combine both in a sort of dynamic inheritance:

abstract class DelegatingSemantics implements Semantics {
    private final Semantics delegate;

    public DelegatingSemantics(Semantics delegate) {
        this.delegate = delegate;
    }

    @Override
    public Memory initial()              { return delegate.initial(); }

    @Override
    public void forward(Memory memory)   { delegate.forward(memory); }

    @Override
    public void backward(Memory memory)  { delegate.backward(memory); }

    @Override
    public void increment(Memory memory) { delegate.increment(memory); }

    @Override
    public void decrement(Memory memory) { delegate.decrement(memory); }

    @Override
    public void output(Memory memory)    { delegate.output(memory); }

    @Override
    public void input(Memory memory)     { delegate.input(memory); }

    @Override
    public void repeat(Action<Memory> program, Memory memory) {
        delegate.repeat(program, memory);
    }
}

Envelopes take a delegating letter to which to forward by default the implemented methods; subclasses need only override the methods of interest and let the envelope handle the rest. The initial semantics S0 is, however, fully concrete. It operates on an unbounded memory of machine integers:

class S0 implements Semantics {
    @Override
    public Memory initial()              { return new UnboundedMemory(); }

    @Override
    public void forward(Memory memory)   { memory.next(); }

    @Override
    public void backward(Memory memory)  { memory.prev(); }

    @Override
    public void increment(Memory memory) { memory.set(memory.get() + 1); }

    @Override
    public void decrement(Memory memory) { memory.set(memory.get() - 1); }

    @Override
    public void output(Memory memory) {
        System.out.print((char) (memory.get() & 255));
    }

The input behavior on EOF is to leave the memory untouched:

@Override
    public void input(Memory memory) {
        try {
            final int c = System.in.read();
            if (c != -1) memory.set(c);
        } catch (IOException e) {
            System.err.println(e);
        }
    }

The meaning of repeat is to execute the enclosed program until the current memory cell is zero:

@Override
    public void repeat(Action<Memory> program, Memory memory) {
        int c;
        while ( (c = memory.get()) != 0 )
            program.apply(memory);
    }
}

This interpretation of repeat will probably never change (but consider a non-Turing-complete version of Brainfuck with bounded repetition, e.g. for server-side Core Wars competitions). The first difference, however, is on input:

class S1 extends DelegatingSemantics {
    public S1(Semantics delegate) { super(delegate); }

    @Override
    public void input(Memory memory) {
        try {
            final int c = System.in.read();
            memory.set(c == -1 ? 0 : c);
        } catch (IOException e) {
            System.err.println(e);
        }
    }
}

The S1 interpretation overrides a Semantics so that it sets the current cell to zero on EOF. The other variant is to set it to -1:

class S1_ extends DelegatingSemantics {
    public S1_(Semantics delegate) { super(delegate); }

    @Override
    public void input(Memory memory) {
        try {
            final int c = System.in.read();
            memory.set(c);
        } catch (IOException e) {
            System.err.println(e);
        }
    }
}

The second difference is in the memory cell size, in this case 8-bit-wide:

class S2 extends DelegatingSemantics {
    public S2(Semantics delegate) { super(delegate); }

    @Override
    public void increment(Memory memory) {
        memory.set((memory.get() + 1) & 255);
    }

    @Override
    public void decrement(Memory memory) {
        memory.set((memory.get() - 1) & 255);
    }
}

Although it uses the delegate Semantics's memory, it truncates it on mutation. The third difference is in the organization of the Memory itself:

class S3 extends DelegatingSemantics {
    protected final int length;

    public S3(int length, Semantics delegate) {
        super(delegate);
        this.length = length;
    }

    @Override
    public Memory initial() { return new BoundedMemory(length); }
}

It uses a bounded memory of the size provided, which disallows moving past its bounds. A variation is to wrap around the current cell when reaching either end:

class S3_ extends DelegatingSemantics {
    protected final int length;

    public S3_(int length, Semantics delegate) {
        super(delegate);
        this.length = length;
    }

    @Override
    public Memory initial() { return new CircularMemory(length); }
}

The same code except for the underlying store selected. The Memory interface itself is simple:

interface Memory {
    int get();
    void set(int value);
    void next();
    void prev();
}

The only operations on it are getting and setting the current cell's value and moving it one position in each direction. The implementation of an UnboundedMemory is, however, a bit sophisticated. It uses the standard Turing Machine trick of simulating a doubly-infinite tape with two semi-infinite ones:

class UnboundedMemory implements Memory {
    private final List<Integer> left  = new ArrayList<Integer>();
    private final List<Integer> right = new ArrayList<Integer>();
    private int cursor;

The right tape contains cells with index 0, 1, 2… while the left tape contains cells indexed by -1, -2, -3… Initially only the zero-th cell exists:

public UnboundedMemory() {
        right.add(0);
        cursor = 0;
    }

The class maintains the invariant that the current cell, to which cursor points, always exists:

@Override
    public int get() {
        if (cursor < 0)
            return left.get(-1 - cursor);
        else
            return right.get(cursor);
    }

    @Override
    public void set(int value) {
        if (cursor < 0)
            left.set(-1 - cursor, value);
        else
            right.set(cursor, value);
    }

New cells are created on demand on the appropriate tape upon cursor movement:

@Override
    public void next() {
        cursor++;
        if (cursor >= 0 && right.size() == cursor)
            right.add(0);
    }

    @Override
    public void prev() {
        --cursor;
        if (cursor < 0 && left.size() == -1 - cursor)
            left.add(0);
    }
}

A BoundedMemory is, by contrast, much simpler:

class BoundedMemory implements Memory {
    protected final int[] tape;
    protected int cursor;

    public BoundedMemory(int length) {
        this.tape = new int[length];
        cursor = 0;
    }

    @Override
    public int get() {
        return tape[cursor];
    }

    @Override
    public void set(int value) {
        tape[cursor] = value;
    }

The only intelligence required is in avoiding moving the cursor outside its bounds:

@Override
    public void next() {
        if (cursor != tape.length - 1)
            cursor++;
    }

    @Override
    public void prev() {
        if (cursor != 0)
            --cursor;
    }
}

A CircularMemory is just a BoundedMemory with a different out-of-bounds behavior:

class CircularMemory extends BoundedMemory {
    public CircularMemory(int length) {
        super(length);
    }

    @Override
    public void next() {
        cursor++;
        if (cursor == tape.length)
            cursor = 0;
    }

    @Override
    public void prev() {
        if (cursor == 0)
            cursor = tape.length;
        --cursor;
    }
}

tl; dr: writing interpreters in Java is tedious. Interestingly enough, I find the object-oriented expression of the Semantics over the different types of Memory very natural, more so even than what modular programming allows. The downsides I find, at least for Java, are two:

1. The sheer amount of boilerplate necessary to express the problem. Even allowing for the lack of closures, algebraic data types and pattern matching, it lacks an automatic delegation mechanism. This is actually a shortcoming of every mainstream object-oriented language (and no, metaprogramming is not a substitute for a language construct that can be checked and verified statically for a number of properties that run-time reflection would not)
2. The need to name everything. Nominal type disciplines not only suck on principle, they actually encourage naming trivial program constructs (classes, interfaces, methods) that therefore take an artificial existence of their own, bloating (module) interfaces and opening new ports for coupling

Still with me? Let me thank you and express my admiration for your fortitude.

Modular Semantics for Brainfuck

The problem with Brainfuck is that its semantics are given by its different implementations but not all its implementations agree so that writing an interpreter is straightforward but writing portable Brainfuck programs is not. OCaml functors allows playing with pluggable semantics in a way that would be very difficult laborious with other languages. I can't imagine this flexibility in object-oriented languages like Java or Python, but in OCaml the mix-and-match approach with module inclusion is straightforward.

Update: OK, so reddit justly challenged my grandstanding. The moral equivalent of this typesafe, modular, extensible interpreter requires more than 520 tight lines, of which 270 go to the parser, pretty-printer and the evaluator (two visitors over 7 case classes), and 250 go to the plug-in semantics. The end result is more flexible than the following OCaml code, since I can choose the composition dynamically, at run-time:

public static void main(String[] args) {
  String hello =
">+++++++++[<++++++++>-]<.>+++++++[<++++>-]<+.+++++++..+++.>>>++++++++[<++++>-]"+
"<.>>>++++++++++[<+++++++++>-]<---.<<<<.+++.------.--------.>>+.";

  Semantics s = new S3_(5000, new S2(new S1_(new S0())));
  Brainfuck bf = new Brainfuck(s);
  bf.evaluate(bf.parse(hello), s.initial());
}

The key is using delegation instead of inheritance to override behavior and spending six hours typing code like a madman.

The language is defined by the effect that its eight instructions have on a memory:

module type SEMANTICS = sig
  type mem
  val mem       : mem
  val forward   : mem -> mem
  val backward  : mem -> mem
  val increment : mem -> mem
  val decrement : mem -> mem
  val output    : mem -> mem
  val input     : mem -> mem
  val repeat    : (mem -> mem) -> (mem -> mem)
end

The initial state of the memory is given by mem. The next six functions correspond directly to the six instructions > < + - . , while the operational semantics of each of the brackets is consolidated into a single small-step function, repeat, so that for a properly balanced Brainfuck program [P] its effect on mem is repeat P mem.

Given a SEMANTICS, the interpretation of a Brainfuck program is straightforward:

module Brainfuck (S : SEMANTICS) = struct

The program is represented by an abstract syntax comprising of a sequence of instructions mapping one-to-one to the surface syntax of the language, except for the pair of brackets that represents a single unit of repetition:

type instr = Fwd | Bak | Inc | Dec | Out | Inp | Rep of program
  and program = instr list

Note: The fact that properly balanced [ and ] denote a repeating computation can be taken as a definition. The translation from concrete syntax to abstract syntax ensures that the mapping is faithful and the operational semantics given for [ and ] as separate instructions corresponds to the one for Rep.

Since the semantics of each instruction is a function from memory to memory, the semantics of a program is the left-to-right composition of the semantics of the individual instructions comprising it:

let rec eval p t = List.fold_left (fun t -> function
  | Fwd   -> S.forward   t
  | Bak   -> S.backward  t
  | Inc   -> S.increment t
  | Dec   -> S.decrement t
  | Out   -> S.output    t
  | Inp   -> S.input     t
  | Rep p -> S.repeat (eval p) t) t p

The translation from concrete to abstract syntax is given by a parser:

let parse str =
    let syntax_err fmt = Printf.kprintf failwith fmt in
    let res = ref []
    and stk = ref [] in
    let emit  i  = res := i :: !res
    and enter () = stk := !res :: !stk; res := []
    and leave () = match !stk with
    | r :: s -> stk := s; res := Rep (List.rev !res) :: r
    | []     -> syntax_err "unmatched `]'"
    in String.iter (function
    | '>' -> emit Fwd
    | '<' -> emit Bak
    | '+' -> emit Inc
    | '-' -> emit Dec
    | '.' -> emit Out
    | ',' -> emit Inp
    | '[' -> enter ()
    | ']' -> leave ()
    |  _  -> ()) str;
    if !stk != [] then syntax_err "unmatched `['" else
    List.rev !res

Only the concrete instructions > < + - . , [ and ] have meaning in a program; all other possible characters are ignored and [ and ] must be properly balanced. An adjoint pretty-printer or formatter translates abstract syntax back to concrete, such that for all abstract programs P, parse (format P) ≡ P:

let format prog =
    let buf = Buffer.create 72
    and len = ref 0 in
    let putc c =
      if !len == 72 || c == '\n' then begin
        Buffer.add_char buf '\n';
        len := 0
      end;
      if c != '\n' then begin
        Buffer.add_char buf c;
        incr len
      end
    in
    let rec go prog = List.iter (function
    | Fwd   -> putc '>'
    | Bak   -> putc '<'
    | Inc   -> putc '+'
    | Dec   -> putc '-'
    | Out   -> putc '.'
    | Inp   -> putc ','
    | Rep p -> putc '['; go p; putc ']') prog
    in go prog; putc '\n'; Buffer.contents buf
end

(The proof of this last property would go by mutual induction on format and parse if it were not that they are imperative; the conversion to pure recursive form is straightforward and mechanical but left as an exercise to the reader.) It is time to give concrete semantics for each of the instructions.

The simplest possible store is a tape of memory cells which can be conveniently represented by a zipper:

type tape = Tape of int list * int * int list

The initial memory has an infinite number of zeros:

module S0 = struct
  type mem = tape

  let mem =
    let rec zeros = 0 :: zeros in
    Tape (zeros, 0, zeros)

Advancing and retreating the cell pointer simply moves the zipper, since both ends are infinite:

let forward  (Tape (ls, c, r :: rs)) = Tape (c :: ls, r, rs)
  let backward (Tape (l :: ls, c, rs)) = Tape (ls, l, c :: rs)

(The cyclic lists at both ends can be considered as sentinel nodes.) The simplest representation for a cell is as the underlying machine integer:

let increment (Mem (ls, c, rs)) = Mem (ls, c + 1, rs)
  let decrement (Mem (ls, c, rs)) = Mem (ls, c - 1, rs)

Character output is consistently among implementations just the output to console of the cell value as an ASCII code:

let output (Mem (_, c, _) as t) =
    output_char stdout (char_of_int (c land 255));
    t

Character input differs on the treatment of end-of-file; probably the most general behavior is to not modify the cell on EOF:

let input (Mem (ls, c, rs) as t) =
    let c = try int_of_char (input_char stdin) with End_of_file -> c in
    Tape (ls, c, rs)

Repetition is the effect of p whenever the current cell is not zero:

let rec repeat p t = match t with
  | Mem (_, 0, _) -> t
  | _             -> repeat p (p t)
end

One variation between interpreters is the EOF behavior. Some of them set the current cell to 0 on EOF:

module S1 (S : SEMANTICS with type mem = tape) = struct
  include S

  let input (Tape (ls, c, rs)) =
    let c = try int_of_char (input_char stdin) with End_of_file -> 0 in
    Tape (ls, c, rs)
end

Others set it to -1:

module S1' (S : SEMANTICS with type mem = tape) = struct
  include S

  let input (Tape (ls, c, rs)) =
    let c = try int_of_char (input_char stdin) with End_of_file -> -1 in
    Tape (ls, c, rs)
end

Another variation between interpreters is the cell width in bytes. The standard reference interpreter uses eight-bit cells:

module S2 (S : SEMANTICS with type mem = tape) = struct
  include S

  let increment (Tape (ls, c, rs)) = Tape (ls, (c + 1) land 255, rs)
  let decrement (Tape (ls, c, rs)) = Tape (ls, (c - 1) land 255, rs)
end

(To avoid redefining all functions I simply mask off excess bits from the native integer representation.) Yet another possible variation is to have a fixed-size tape. What to do when trying to move the cell pointer past the ends is a free choice; I could opt for simply ignoring the attempted movement:

let fill v =
  let rec go l n =
    if n == 0 then l else
    go (v :: l) (pred n)
  in go []

module S3 (N : sig val size : int end)
          (S : SEMANTICS with type mem = tape) = struct
  include S

  let mem = Tape ([], 0, fill 0 N.size)

  let forward  t = match t with
  | Tape (ls, c, r :: rs) -> Tape (c :: ls, r, rs)
  | Tape (_ , _, []     ) -> t

  let backward t = match t with
  | Tape (l :: ls, c, rs) -> Tape (ls, l, c :: rs)
  | Tape ([]     , _, _ ) -> t
end

The other alternative is to wrap the cell pointer at either end:

module S3' (N : sig val size : int end)
           (S : SEMANTICS with type mem = tape) = struct
  include S3 (N) (S)

  let forward  t = match t with
  | Tape (ls, c, r :: rs) -> Tape (c :: ls, r, rs)
  | Tape (ls, c, []     ) ->
    let r :: rs = List.rev (c :: ls) in
    Tape ([], r, rs)

  let backward t = match t with
  | Tape (l :: ls, c, rs) -> Tape (ls, l, c :: rs)
  | Tape ([]     , c, rs) ->
    let l :: ls = List.rev (c :: rs) in
    Tape (ls, l, [])
end

Now the choice of semantics is a matter of stacking the desired functors:

let hello = "
>+++++++++[<++++++++>-]<.>+++++++[<++++>-]<+.+++++++..+++.>>>++++++++[<++++>-]
<.>>>++++++++++[<+++++++++>-]<---.<<<<.+++.------.--------.>>+."

let _ =
  let module S  = S3'(struct let size = 5000 end)(S2(S1(S0))) in
  let module BF = Brainfuck(S) in
  BF.(eval (parse hello)) S.mem

This makes BF a Brainfuck interpreter running on a bounded memory of 5.000 byte-sized cells with 0 on EOF.

Yield, Continue

Roshan P. James and Amr Sabry show in "Yield: Mainstream Delimited Continuations" the interdefinability of yield-style generators and delimited continuations. Their encoding is at the same time simple and general, and even if the examples given in the paper are in Haskell, their translation into OCaml is straightforward. So much so that the result is essentially equivalent to ASAI Kenichi's OchaCaml (Edit: this claim of mine is certainly unsubstantiated and quite possibly wrong. See Zerny's comment).

James and Sabry generalize the mechanics of yield to a three-ported construct represented by the type (ι, ο, ρ) Yield:

This type encapsulates the communication between an iterator and its calling context, where the iterator yields values of type ο, receives inputs of type ι and terminates (or returns) with a final result of type ρ. This communication is mediated by a delimited context that can be activated with run which … marks the boundary of an iterator and delimits the action of yield. This communication is effected by a reified continuation given by a concrete data type with which the calling context can interact:

type ('i, 'o, 'r) iterator =
| Result of 'r
| Susp of 'o * ('i -> ('i, 'o, 'r) iterator)

In effect, run converts a monadic producer that uses yield into a CPS-transformed consumer that invokes the continuation given by an iterator. These patterns of interaction can be abstracted somewhat. The most general consumer is given by foreach:

let rec foreach (m : ('i, 'o, 'r) iterator) (f : 'o -> 'i) : 'r = match m with
| Susp (v, k) -> foreach (k (f v)) f
| Result r    -> r

It applies f to each value yielded by the iterator, feeding the result back to it. If the consumer is interested just in the yielded values and not in the result of the iteration, it can fold over them:

let rec fold (m : ('i, 'i, 'r) iterator) (f : 'i -> 'j -> 'j) (e : 'j) : 'j = match m with
| Susp (v, k) -> f v (fold (k v) f e)
| Result _    -> e

The essence of the iterator is given by an abstract signature:

module type YIELD = sig
  type ('i, 'o, 'r) yield
  val return : 'r -> ('i, 'o, 'r) yield
  val (>>=) : ('i, 'o, 'r) yield -> ('r -> ('i, 'o, 's) yield) -> ('i, 'o, 's) yield
  val yield : 'o -> ('i, 'o, 'i) yield
  val run : ('i, 'o, 'r) yield -> ('i, 'o, 'r) iterator
end

which gives a multi-parameter monad together with a pair of operations: yield, that returns a computation returning the yielded value (note the difference with return); and run, that captures the computation's context and reifies it into an iterator. The paper gives two possible implementations. The first "grabs" each invocation frame turning it directly into an iterator:

module FrameGrabbingYield : YIELD = struct
  type ('i, 'o, 'r) yield = ('i, 'o, 'r) iterator

  let return e = Result e

  let rec (>>=) m f = match m with
  | Result v    -> f v
  | Susp (v, k) -> Susp (v, fun x -> k x >>= f)

  let yield v = Susp (v, return)

  let run e = e
end

The seconds uses the CPS-encoded delimited continuation monad directly:

module CPSYield : YIELD = struct
  type ('i, 'o, 'r) yield =
    { cont : 'b . ('r -> ('i, 'o, 'b) iterator) -> ('i, 'o, 'b) iterator }

  let return x = { cont = fun k -> k x }

  let (>>=) m f = { cont = fun k -> m.cont (fun x -> (f x).cont k) }

  let yield v = { cont = fun k -> Susp (v, k) }

  let run e = e.cont (fun r -> Result r)
end

This is the standard CPS monad with answer type polymorphism, as given by Kiselyov. Now yield e is shift $ return . Susp e, and run e is equivalent to reset $ e >>= return . Result). This is sufficient but a bit bare-bones. Let's build from here:

module YieldT (Y : YIELD) = struct
  include Y

In the simplest case, generators simply yield successive values. The result of the computation is the value itself, that can be updated for the next cycle:

let rec repeat x = yield x >>= repeat
  let rec from i = yield i >>= fun j -> from (succ j)

Transformers are a bit more involved in that they must consume the iterator and yield new values, in effect delimiting the control of the iterator they consume. The simplest transformer is obviously map:

let rec map f y =
    let rec go = function
    | Result r    -> return r
    | Susp (v, k) -> yield (f v) >>= fun _ -> go (k v)
    in go (run y)

(Note that the monadic fmap would only act on the result and not on the generated values.) In this case, the result of the computation is the mapped value of the original iterator, that must be continued with the original value. Truncating an iterator is straightforward:

let rec take n y =
    let rec go n = function
    | Result r -> return (Some r)
    | Susp (_, _) when n = 0 -> return None
    | Susp (v, k) -> yield v >>= fun x -> go (n - 1) (k x)
    in go n (run y)

Combining two generators is also straightforward:

let zip y1 y2 =
    let rec go = function
    | Result r1, Result r2 -> return (r1, r2)
    | Susp (v1, k1), Susp (v2, k2) ->
      yield (v1, v2) >>= fun (x1, x2) -> go (k1 x1, k2 x2)
    | _ -> failwith "zip"
    in go (run y1, run y2)
end

(Iterators that return early must be dealt with in a somewhat arbitrary way.) With this it is relatively straightforward to use iterators:

let ex1 y =
  let module Y = YieldT( (val y : YIELD) ) in
  foreach Y.(run (take 10 (map succ (from 0)))) (Printf.printf "%d ")

And both implementations give equivalent results:

# let _ = ex1 (module FrameGrabbingYield : YIELD) ;;
1 2 3 4 5 6 7 8 9 10 - : 'a option = None
# let _ = ex1 (module CPSYield : YIELD) ;;
1 2 3 4 5 6 7 8 9 10 - : 'a option = None

Furthermore, Asai's examples (as given in this Reddit thread) can be easily duplicated as well:

module Tree (Y : YIELD) = struct
  type 'a tree = E | N of 'a tree * 'a * 'a tree

  open Y

  let rec depth_walk : 'a tree -> ('b, 'a, 'b tree) yield = function
  | N (l, n, r) ->
    depth_walk l >>= fun l' ->
    yield n      >>= fun n' ->
    depth_walk r >>= fun r' ->
    return (N (l', n', r'))
  | E -> return E

  let to_list t = fold (run (depth_walk t)) (fun x xs -> x :: xs) []

  let map f t = foreach (run (depth_walk t)) f

  let samefringe l r =
    let rec visit l r = match l, r with
    | Result _, Result _ -> true
    | Susp (a, ka), Susp (b, kb)
      when a = b ->
      visit (ka a) (kb b)
    | _ -> false
    in visit (run (depth_walk l)) (run (depth_walk r))

  let swap l r =
    let rec visit l r = match l, r with
    | Susp (a, ka), Susp (b, kb) -> visit (ka b) (kb a)
    | Result t1, Result t2 -> (t1, t2)
    | _ -> failwith "Unequal number of leaves"
    in visit (run (depth_walk l)) (run (depth_walk r))
end

Note that, except for the return type polymorphism, these versions are exactly the same. To prove that all works properly, here are a number of tests:

# module T = Tree(CPSYield) ;;
# open T ;;

# let t1 = N (N (E, 10, E), 20, N (E, 30, N (E, 40, E)))
and t2 = N (N (E, 10, N (E, 20, E)), 30, N (E, 40, E))
and t3 = N (N (E, 'a', N (E, 'b', E)), 'c', N (E, 'd', E))
;;

(I omit the output of these for clarity.)

# let _ = map succ t1 ;;
- : int T.tree = N (N (E, 11, E), 21, N (E, 31, N (E, 41, E)))
# let _ = to_list t1 ;;
- : int list = [10; 20; 30; 40]
# let _ = samefringe t1 t2 ;;
- : bool = true
# let _ = swap t1 t3 ;;
- : char T.tree * int T.tree =
(N (N (E, 'a', E), 'b', N (E, 'c', N (E, 'd', E))),
 N (N (E, 10, N (E, 20, E)), 30, N (E, 40, E)))

Note that in the last example the trees retain their respective shapes but interchange the values of their leaves.

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.

Polymorphic recursion with rank-2 polymorphism in OCaml 3.12

Using polymorphic recursion in OCaml just got easy and direct! With the new syntax, Okasaki's binary random-access lists translate to OCaml 3.12 practically verbatim, without the need for cumbersome encodings. You should refer to the book (Purely Functional Data Structures, p. 147) for comparison, but here's the implementation in its entirety:

type 'a seq = Nil | Zero of ('a * 'a) seq | One of 'a * ('a * 'a) seq

let nil = Nil

let is_empty = function Nil -> true | _ -> false

let rec cons : 'a . 'a -> 'a seq -> 'a seq =
  fun x l -> match l with
  | Nil         -> One (x, Nil)
  | Zero    ps  -> One (x, ps)
  | One (y, ps) -> Zero (cons (x, y) ps)

let rec uncons : 'a . 'a seq -> 'a * 'a seq = function
| Nil          -> failwith "uncons"
| One (x, Nil) -> x, Nil
| One (x, ps ) -> x, Zero ps
| Zero    ps   ->
  let (x, y), qs = uncons ps in
  x, One (y, qs)

let head l = let x, _  = uncons l in x
and tail l = let _, xs = uncons l in xs

let rec lookup : 'a . int -> 'a seq -> 'a =
  fun n l -> match l with
  | Nil                    -> failwith "lookup"
  | One (x, _ ) when n = 0 -> x
  | One (_, ps)            -> lookup (n - 1) (Zero ps)
  | Zero ps                ->
    let (x, y) = lookup (n / 2) ps in
    if n mod 2 = 0 then x else y

let update n e =
  let rec go : 'a . ('a -> 'a) -> int -> 'a seq -> 'a seq =
    fun f n l -> match l with
    | Nil                    -> failwith "update"
    | One (x, ps) when n = 0 -> One (f x, ps)
    | One (x, ps)            -> cons x (go f (n - 1) (Zero ps))
    | Zero ps                ->
      let g (x, y) = if n mod 2 = 0 then (f x, y) else (x, f y) in
      Zero (go g (n / 2) ps)
  in go (fun x -> e) n

The implementation given in the book is rather bare-bones, but it can be extended with some thought and by paying close attention to the techniques Okasaki uses. To begin with, a length function is a very simple O(log n) mapping from constructors to integers:

let rec length : 'a . 'a seq -> int
  = fun l -> match l with
  | Nil         -> 0
  | Zero ps     ->     2 * length ps
  | One (_, ps) -> 1 + 2 * length ps

It is also rather easy to write a map for binary random-access lists:

let rec map : 'a 'b . ('a -> 'b) -> 'a seq -> 'b seq =
  fun f l -> match l with
  | Nil          -> Nil
  | One (x,  ps) -> One (f x, map (fun (x, y) -> (f x, f y)) ps)
  | Zero ps      -> Zero     (map (fun (x, y) -> (f x, f y)) ps)

Note two things: first, that both parameters need to be generalized as both the argument and the return type vary from invocation to invocation, as shown by the Zero case. Second, that there is no need to use cons, as map preserves the shape of the list. With this as a warm-up, writing fold_right is analogous:

let rec fold_right : 'a 'b . ('a -> 'b -> 'b) -> 'a seq -> 'b -> 'b =
  fun f l e -> match l with
  | Nil          -> e
  | One (x, ps)  -> f x (fold_right (fun (x, y) z -> f x (f y z)) ps e)
  | Zero ps      ->      fold_right (fun (x, y) z -> f x (f y z)) ps e

Given a right fold, any catamorphism is a one-liner:

let append l = fold_right cons l

let of_list l = List.fold_right cons l nil
and to_list l = fold_right (fun x l -> x :: l) l []

Now, armed with fold_right, filling up a list library is easy; but taking advantage of the logarithmic nature of the representation requires thought. For instance, building a random-access list of size n can be done in logarithmic time with maximal sharing:

let repeat n x =
  let rec go : 'a . int -> 'a -> 'a seq = fun n x ->
     if n = 0 then Nil else
  if n = 1 then One (x, Nil) else
     let t = go (n / 2) (x, x) in
     if n mod 2 = 0 then Zero t else One (x, t)
  in
  if n < 0 then failwith "repeat" else go n x

By analogy with binary adding, there is also a fast O(log n) merge:

let rec merge : 'a . 'a seq -> 'a seq -> 'a seq =
  fun l r -> match l, r with
  | Nil        ,         ps
  |         ps , Nil         -> ps
  | Zero    ps , Zero    qs  -> Zero (merge ps qs)
  | Zero    ps , One (x, qs)
  | One (x, ps), Zero    qs  -> One (x, merge ps qs)
  | One (x, ps), One (y, qs) -> Zero (cons (x, y) (merge ps qs))

It walks both lists, "adding" the "bits" at the head. The only complication is the case where both lists are heded by two Ones, which requires rippling the carry with a call to cons. An alternative is to explicitly keep track of the carry, but that doubles the number of branches. This merge operation does not preserve the order of the elements on both lists. It can be used, however, as the basis for a very fast nondeterminism monad:

let return x = One (x, Nil)
let join mm  = fold_right merge mm Nil
let bind f m = join (map f m)

let mzero = Nil
let mplus = merge

The rank-2 extension to the typing algorithm does not extend to signatures, as in Haskell. It only has effect on the typing of the function body, by keeping the type parameter fresh during unification, as the signature of the module shows:

type 'a seq = Nil | Zero of ('a * 'a) seq | One of 'a * ('a * 'a) seq
val nil : 'a seq
val is_empty : 'a seq -> bool
val cons : 'a -> 'a seq -> 'a seq
val uncons : 'a seq -> 'a * 'a seq
val head : 'a seq -> 'a
val tail : 'a seq -> 'a seq
val lookup : int -> 'a seq -> 'a
val update : int -> 'a -> 'a seq -> 'a seq
val length : 'a seq -> int
val map : ('a -> 'b) -> 'a seq -> 'b seq
val fold_right : ('a -> 'b -> 'b) -> 'a seq -> 'b -> 'b
val append : 'a seq -> 'a seq -> 'a seq
val of_list : 'a list -> 'a seq
val to_list : 'a seq -> 'a list
val repeat : int -> 'a -> 'a seq
val merge : 'a seq -> 'a seq -> 'a seq
val return : 'a -> 'a seq
val join : 'a seq seq -> 'a seq
val bind : ('a -> 'b seq) -> 'a seq -> 'b seq
val mzero : 'a seq
val mplus : 'a seq -> 'a seq -> 'a seq

To use rank-2 types in interfaces it is still necessary to encode them via records or objects.

Properly Bound

To all practitioners: the type of bind is not the type of >>=. For a monad α m, the latter has type:

val (>>=) : α m → (α → β m) → β m

only because >>= is used as a combinator that allows pipelining computations from left to right, as per usual convention:

… m >>= fun x →
  n >>= fun y →
  …
  return f x y

On the other hand, if you want to take maximum advantage of the Theorems for Free! then your bind should have type:

val bind : (α → β m) → (α m → β m)

because it is a natural transformation, together with return:

val return : α → α m

You can see immediately how both "fit" together; in particular, the second monad law (right identity) falls off naturally (!) from the types:

bind return ≡ id

The first monad law (left identity) is also immediately natural:

bind f ∘ return ≡ f

since bind f's domain coincides with return's range by inspection. The third monad law (associativity) is much less regular but you can see a hint of the mechanics of adjointedness if you read bind g as a whole:

bind g ∘ bind f ≡ bind (bind g ∘ f)

This note is motivated by a reading of Jérémie Dimino's slides about Jérôme Vouillon's Lwt, specifically slide 6 (Edit: thanks Gabriel for the heads up about proper attribution).

GADTs for the Rest of Us

In a nutshell, generalized algebraic data types, or GADTs for short, are a first-class phantom type of sorts. The basic idea is to enrich the constructors of an ADT with a more expressive "return" type by allowing the instantiation of one or more type parameters. A simple motivating example is that of an abstract syntax in Peyton Jones's original paper:

data Term a where
  Lit  :: Int        -> Term Int
  Inc  :: Term Int   -> Term Int
  IsZ  :: Term Int   -> Term Bool
  If   :: Term Bool  -> Term a    -> Term a     -> Term a
  Pair :: Term a     -> Term b    -> Term (a,b)
  Fst  :: Term (a,b) -> Term a
  Snd  :: Term (a,b) -> Term b

For instance, the constructor for Inc specifies the type of its argument as Term Int by constraining its application to bind the parameter a to Int, in effect specifying the "return type" of the constructor. Xavier Leroy's proposal for a syntax extension of OCaml would look like this:

type 'a term =
| Lit  of int                            constraint 'a = int
| Inc  of int term                       constraint 'a = int
| IsZ  of int term                       constraint 'a = bool
| If   of bool term * 'a term * 'a term
| Pair of  'b  term * 'c term            constraint 'a = 'b * 'c
| Fst  of ('b * 'c) term                 constraint 'a = 'b
| Snd  of ('b * 'c) term                 constraint 'a = 'c

Each syntax emphasizes complementary views of what "is" the essence of this generalization: Haskell's makes clear the parameter's functional dependency on the constructor; OCaml's stresses the constraints placed on a match on the constructor. In any case, this type shows the three cases a GADT might present:

• No constraint, as in the constructor If
• A concrete constraint, as in the constructors Lit, Inc or IsZ
• An existential constraint, as in the constructors Pair, Fst or Snd

The constraints a GADT places on the parameters must be met by the functions that do a pattern-matching on the type. In general, the result type is a function of the types of the parameter. This requires polymorphic recursion which forces the use of an explicit rank-2 type for it. For instance, a function evaluating a Term a will have type a for each possible a defined in the GADT. In the following code the match for Lit forces a to be instantiated to Int, whereas the matching for IsZ forces it to Bool:

eval :: Term a -> a
eval term = case term of
  Lit n    -> n
  Inc t    -> eval t + 1
  IsZ t    -> eval t == 0
  If c x y -> if eval c then eval x else eval y
  Pair x y -> (eval x, eval y)
  Fst t    -> fst (eval t)
  Snd t    -> snd (eval t)

Unfortunately, the current version of OCaml (3.11) does not yet include either GADTs or rank-2 polymorphism. On July 11th, 2009, Oleg announced that OCaml's type system is expressive enough to encode GADTs. On his site he shows three applications of the technique. However, Oleg's examples do not offer much guidance in how to apply the encoding, especially since the more complete example, that of the typed printf/scanf, is too advanced an application to use as a template. I have shown in another post how to encode polymorphic recursion with rank-2 types. Here I'll explain how to treat each of the three cases in a GADT to systematically embed the type in OCaml.

The basic technique is to use a witness for the constraint placed on the parameter. Oleg uses a module with the required semantics:

module EQ = struct
  type ('a,'b) eq = Refl of 'a option ref * 'b option ref

  let refl () = let r = ref None in Refl (r, r)

  let symm (Refl (x, y)) = Refl (y, x)

  let apply_eq (Refl (x, y)) v =
    x := Some v;
    match !y with
  | Some w -> x := None; w
  | _      -> assert false
end

A value eq of type ('a, 'b) eq witnesses the equality of types a and b. Given such a witness and a value x of type a, apply_eq eq x is a safe type cast of x to type b. This is sufficient to force the constraints on the type parameter, as explained in the paper Oleg references. For each one of the above identified cases, Oleg's code encodes the constructor, defines a smart constructor to ease the use of the type as an embedded DSL and pattern-matches on the constructor in order to access its parameters. This is how:

• For unconstrained constructors, nothing needs to be done.

  For instance, the type constructor for If does not require fixing the constructor's parameter a as it is by definition equal to the type parameter:

  | If of bool term * 'a term * 'a term
  

  A smart constructor for this constructor is routine:

  let if_ c t f = If (c, t, f)
  

  (the underscore is to avoid a clash with the reserved keyword). Equally routine is pattern-matching on it:

  | If (c,t,f) -> …
  

  If desired for reasons of regularity, however, the constraint 'a = 'b for an existentially-qualified parameter b can be introduced explicitely using the last encoding.

• For concretely-constrained constructors, it is necessary to witness the equality of the parameter and this concrete type.

  It is not as simple, however, to augment the constructor with a value of type ('a, t) EQ.eq: since matches on those values would force the type of a to be the same for every match, it would require that t be the same concrete type everywhere. What is needed instead is an existential type, say b such that it is constrained to be t and which in turn constrains a. Oleg encodes the existential with the double negation on a rank-2 universal, by way of a witness type. In order to maximize the compactness of the code, he uses a class type to introduce the required rank-2 type:

  | Lit of < m_lit : 'w . ((int, 'a) eq -> int -> 'w) -> 'w >
  

  Here w witnesses the existence of an a such that, if successfully constrained to int, it would bear the required type int term. A smart constructor for this constructor must build the object instance which will provide the required witness:

  let lit n = Lit (object
    method m_lit : 'w . ((int, 'a) eq -> int -> 'w) -> 'w =
      fun k -> k (refl ()) n end)
  

  Note first that, under the Curry-Howard isomorphism, continuations encode double negation. Note also that the typing must be explicit since it relies on structual and not nominal class types. Note finally that the encoding style is curried much as in Haskell definitions; it is entirely equivalent to encode Leroy-style tupled constructors.

  Now a match on a constructor of this kind must invoke the method on the object parameter with a suitable continuation that will accept the witness as valid and coerce the argument to the constrained type:

  | Lit o -> o#m_lit (fun eq n -> apply_eq eq n)
  

  As will be apparent from the complete encoding of the Haskell example, the other cases are the same.

• For existentially-constrained constructors, it is necessary to encode the existential with a rank-2 type, and witness the equality of the parameter and this type.

  This case is an extension of the previous one, with the twist that the existential must be encoded separately. In this case Oleg uses a record type instead of an object type, but the encoding could use the latter equally well. For instance, in the case of Pairs, there must exist types b and c such that a is constrained to be b×c. The constructor factors out this existential:

  | Pair of < m_pair : 'w . ('a, 'w) k_pair -> 'w >
  

  Here, k_pair will bear the required witness w on a's constraint:

  type ('a, 'w) k_pair = { k_pair : 'b 'c . ('b*'c, 'a) eq -> 'b term -> 'c term -> 'w }
  

  The equality witness expresses the required intent on the types of the constructor's arguments. The smart constructor is analogous to the previous one, except that in this case the continuation has type k_pair:

  let pair p q = Pair (object
    method m_pair : 'w . ('a, 'w) k_pair -> 'w =
      fun k -> k.k_pair (refl ()) p q end)
  

  The pattern-match is analogous too:

  | Pair o -> o#m_pair { k_pair = fun eq x y -> apply_eq eq … }
  

Here's the complete code for the type definitions and the smart constructors encoding the Haskell mini-expression language example:

type 'a term =
| Lit  of < m_lit  : 'w . ((int , 'a) eq -> int -> 'w) -> 'w >
| Inc  of < m_inc  : 'w . ((int , 'a) eq -> int term -> 'w) -> 'w >
| IsZ  of < m_isz  : 'w . ((bool, 'a) eq -> int term -> 'w) -> 'w >
| If   of bool term * 'a term * 'a term
| Pair of < m_pair : 'w . ('a, 'w) k_pair -> 'w >
| Fst  of < m_fst  : 'w . ('a, 'w) k_fst  -> 'w >
| Snd  of < m_snd  : 'w . ('a, 'w) k_snd  -> 'w >
and ('a, 'w) k_pair = { k_pair : 'b 'c . ('b*'c, 'a) eq -> 'b term -> 'c term -> 'w }
and ('a, 'w) k_fst  = { k_fst  : 'b 'c . ('b   , 'a) eq -> ('b * 'c) term -> 'w }
and ('a, 'w) k_snd  = { k_snd  : 'b 'c . ('c   , 'a) eq -> ('b * 'c) term -> 'w }

let lit  n     = Lit  (object
  method m_lit  : 'w . ((int , 'a) eq -> int -> 'w) -> 'w =
    fun k -> k (refl ()) n end)
let inc  t     = Inc  (object
  method m_inc  : 'w . ((int , 'a) eq -> int term -> 'w) -> 'w =
    fun k -> k (refl ()) t end)
let isz  t     = IsZ  (object
  method m_isz  : 'w . ((bool, 'a) eq -> int term -> 'w) -> 'w =
    fun k -> k (refl ()) t end)
let if_  c t f = If   (c, t, f)
let pair p q   = Pair (object
  method m_pair : 'w . ('a, 'w) k_pair -> 'w =
    fun k -> k.k_pair (refl ()) p q end)
let first  p   = Fst  (object
  method m_fst  : 'w . ('a, 'w) k_fst  -> 'w =
    fun k -> k.k_fst  (refl ()) p end)
let second p   = Snd  (object
  method m_snd  : 'w . ('a, 'w) k_snd  -> 'w =
    fun k -> k.k_snd  (refl ()) p end)

It is important to remark on the types of the smart constructors, which are the most similar to the Haskell constructors:

val lit    : int -> int term
val inc    : int term -> int term
val isz    : int term -> bool term
val if_    : bool term -> 'a term -> 'a term -> 'a term
val pair   : 'a term -> 'b term -> ('a * 'b) term
val first  : ('a * 'b) term -> 'a term
val second : ('a * 'b) term -> 'b term

Now, as I mentioned above, an evaluator has type 'a term -> 'a for all a; this requires rank-2 polymorphism. In order to keep the namespace tidy, I use a local module definition hiding a record type encoding the higher-kinded function type:

let eval e =
  let module E = struct
    type eval = { eval : 'a . 'a term -> 'a }
    let rec eval = { eval = function
    | Lit  o      -> o#m_lit  (fun eq n -> apply_eq eq n)
    | Inc  o      -> o#m_inc  (fun eq t -> apply_eq eq (eval.eval t + 1))
    | IsZ  o      -> o#m_isz  (fun eq t -> apply_eq eq (eval.eval t = 0))
    | If  (c,t,f) -> if eval.eval c then eval.eval t else eval.eval f
    | Pair o      ->
      o#m_pair { k_pair = fun eq x y -> apply_eq eq (eval.eval x, eval.eval y) }
    | Fst  o      ->
      o#m_fst  { k_fst  = fun eq p   -> apply_eq eq (fst (eval.eval p)) }
    | Snd  o      ->
      o#m_snd  { k_snd  = fun eq p   -> apply_eq eq (snd (eval.eval p)) }
    }
  end in E.eval.E.eval e

In every case the coercion must be applied at the end, to the result of recursively evaluating the subexpressions in a constructor.

This is all there is to Oleg's encoding. For me, this exegesis has two lessons: first, much as rank-2 polymorphism, GADTs are a conservative extension to Haskell's and OCaml's type system. In fact, version 3.12 will allow higher-ranked functions via explicit annotations. One can only hope that the latter would also find its way into the next release. Second, that Oleg's proof-of-concept examples bear detailed examination to find the general mechanism behind his insights.

Fun with (Type) Class

I'd like to motivate OCaml's object-oriented features (the "O" in "OCaml") by showing an encoding of (first-order) Haskell type classes. This will require making use of almost everything in OCaml's object buffet: class types, virtual classes, inheritance of class types and of classes, double dispatch and coercion.

Haskell could be said to have the best type system among all languages in wide use at the moment, striking a delicate balance between power and practicality without compromising purity (neither conceptual nor functional). In the words of Oleg Kiselyov, it sports "attractive types". A great feature is the presence of type-indexed values via the type-class mechanism. In a nutshell, type-indexed values are functions from types to values. A classic example is overloaded operators, where for instance the same symbol + denotes addition over the integers, floating-point and rational numbers, depending on the type of its parameters. Haskell provides "type magic" to automatically infer the intended function (the value) based on the types of the arguments to which it is applied, achieving a form of type-safe "ad-hoc" polymorphism.

The ML family of languages doesn't have the machinery to attain such expressive power. There are, however, a number of ways to encode type-indexed families with an explicit parameter encoding the selector type. The oldest, and most complicated technique is that of Danvy (see also this complete example) which is not really equivalent to Haskell's type classes but a sophisticated application of phantom types. Another technique is using an explicit dictionary (Yaron Minsky has a worked example) from which to select the appropriate operation. Normally these dictionaries are records; the labels provide type-safe instantiation of the generic value family. The problem with records is that they are not extensible, so it is not immediate how to encode the equivalent of inheritance of type classes. OCaml's object-oriented sublanguage is especially well-suited for the task, allowing for a natural encoding that shows that the "class" in Haskell's "type classes" is more object-oriented than it seems at first sight.

I'll start with a bit of Haskell's standard prelude, as shown in the Report in a nice graph. I'll focus on the two most common nontrivial classes, Eq and Ord. The first is defined as:

class  Eq a  where
    (==), (/=)  ::  a -> a -> Bool

    x /= y  = not (x == y)
    x == y  = not (x /= y)

I encode a Haskell type class in OCaml with… (surprise!) a class type and associated functions:

class type ['a] eq = object
  method equal     : 'a -> 'a -> bool
  method not_equal : 'a -> 'a -> bool
end

Since the type class has a type parameter a, my class type also has a type parameter 'a. Each member of the type class corresponds to a (named) method and to a regular function taking the class type as a dictionary parameter:

let (===) x y (eq : 'a #eq) = eq#equal x y
and (<=>) x y (eq : 'a #eq) = eq#not_equal x y

(I've opted to not shadow the regular operators in Pervasives). The weird order of the parameters (you'd expect the dictionary to come first) is such that I can write:

    if x === y $ eq_int then …

where ($) is the application operator. Haskell provides default implementations for both members; as the Report notes:

This declaration gives default method declarations for both /= and ==, each being defined in terms of the other. If an instance declaration for Eq defines neither == nor /=, then both will loop.

I find that unsettling, so I'll just define one via a virtual class (not class type):

class virtual ['a] eq_base = object (self)
  method virtual equal : 'a -> 'a -> bool
  method not_equal x y = not (self#equal x y)
end

In this case, equal is left virtual. It is important that the class be left virtual even if equal is defined, so that it cannot be instantiated. This means that it cannot be coerced to the class type eq, since it is illegal to shadow virtual members that were declared non-virtual. Now come the instances of the type class. In Haskell, a very simple instance is that for unit which is built-in (via deriving) but could be declared as:

instance  Eq ()  where
    () == () = true

To encode instances, I use an immediate object bound to an identifier:

let eq_unit : unit eq = object
  inherit [unit] eq_base
  method equal     () () = true
  method not_equal () () = false
end

Note the coercion to the corresponding monomorphic instance of the class type. I inherit from the default implementation in the class base, even if in this case I explicitly implement all methods for efficiency. The same encoding works for booleans too:

let eq_bool : bool eq = object
  inherit [bool] eq_base
  method equal     = (==)
  method not_equal = (!=)
end

OCaml has built-in ad-hoc polymorphic comparisons that I could use directly:

class ['a] eq_poly : ['a] eq = object
  inherit ['a] eq_base
  method equal     = Pervasives.(=)
  method not_equal = Pervasives.(<>)
end

With that I can have type classes for the primitive types:

let eq_int    = (new eq_poly :> int    eq)
and eq_float  = (new eq_poly :> float  eq)
and eq_char   = (new eq_poly :> char   eq)
and eq_string = (new eq_poly :> string eq)

Here I instantiate objects of the eq_poly class coerced to the correct monomorphic instance of eq (recall that in OCaml coercion is always explicit). The type class instance for pairs requires type classes for each of its components. In Haskell, we'd have:

instance  (Eq a, Eq b) => Eq ((,) a b)  where …

(not really, but let me gloss over that). Encoding that in OCaml also requires a witness for each type parameter as explicit arguments to the constructor:

let eq_pair (l : 'a eq) (r : 'b eq) : ('a * 'b) eq = object (self)
  inherit ['a * 'b] eq_base
  method equal (p, q) (p', q') = l#equal p p' && r#equal q q'
end

An inefficiency of this encoding is that it creates a new object with every invocation of the witness function. For instance, in general eq_pair eq_unit eq_bool != eq_pair eq_unit eq_bool and so on for every witness. The same is needed to encode an equality witness for option types:

let eq_option (o : 'a eq) : 'a option eq = object
  inherit ['a option] eq_base
  method equal x y = match x, y with
    None  , None   -> true
  | Some x, Some y -> o#equal x y
  | _              -> false
end

And for lists:

let eq_list (o : 'a eq) : 'a list eq = object
  inherit ['a list] eq_base
  method equal =
    let rec equal x y = match x, y with
    | [], [] -> true
    | _ , []
    | [], _  -> false
    | x :: xs, y :: ys when o#equal x y -> equal xs ys
    | _      -> false
    in equal
end

(I use explicit closed recursion for efficiency). In all these cases, I encoded a derived instance via an explicit witness passed as a parameter. Derived type classes require genuine inheritance of class types, as seen in the encoding of Haskell's Ord type class:

class  (Eq a) => Ord a  where
    compare              :: a -> a -> Ordering
    (<), (<=), (>), (>=) :: a -> a -> Bool
    max, min             :: a -> a -> a

(I omit showing the default implementations). I use the SML ordering type for fidelity:

type ordering = LT | EQ | GT

let of_comparison c = if c < 0 then LT else if c > 0 then GT else EQ
and to_comparison   = function LT -> -1 | EQ -> 0 | GT -> -1

The class type encoding the Ord type class is:

class type ['a] ord = object
  inherit ['a] eq
  method compare       : 'a -> 'a -> ordering
  method less_equal    : 'a -> 'a -> bool
  method less_than     : 'a -> 'a -> bool
  method greater_equal : 'a -> 'a -> bool
  method greater_than  : 'a -> 'a -> bool
  method max           : 'a -> 'a -> 'a
  method min           : 'a -> 'a -> 'a
end

Again, operators take an explicit witness as a dictionary:

let (<==) x y (ord : 'a #ord) = ord#less_equal    x y
and (<<<) x y (ord : 'a #ord) = ord#less_than     x y
and (>==) x y (ord : 'a #ord) = ord#greater_equal x y
and (>>>) x y (ord : 'a #ord) = ord#greater_than  x y

And I provide a virtual class with default implementations:

class virtual ['a] ord_base = object (self)
  inherit ['a] eq_base
  method virtual compare : 'a -> 'a -> ordering
  method equal         x y = match self#compare x y with EQ -> true  | _ -> false
  method less_equal    x y = match self#compare x y with GT -> false | _ -> true
  method less_than     x y = match self#compare x y with LT -> true  | _ -> false
  method greater_equal x y = match self#compare x y with LT -> false | _ -> true
  method greater_than  x y = match self#compare x y with GT -> true  | _ -> false
  method max           x y = match self#compare x y with LT -> y | _ -> x
  method min           x y = match self#compare x y with GT -> y | _ -> x
end

Note how the class type inheritance ord :> eq translates into class inheritance ord_base :> eq_base. The instances for unit and bool use inheritance and selective overriding for efficiency:

let ord_unit : unit ord = object
  inherit [unit] ord_base
  method equal     = eq_unit#equal
  method not_equal = eq_unit#not_equal
  method compare () () = EQ
  method max     () () = ()
  method min     () () = ()
end

let ord_bool : bool ord = object
  inherit [bool] ord_base
  method equal     = eq_bool#equal
  method not_equal = eq_bool#not_equal
  method compare b b' = match b, b' with
  | false, true -> LT
  | true, false -> GT
  | _           -> EQ
  method max = (||)
  method min = (&&)
end

In order to profit from the efficient implementation of equal and not_equal I explicitly delegate on the methods in the corresponding eq instances. Now as before I can use the ad-hoc polymorphic operators in Pervasives to speed writing the type classes for atomic types:

class ['a] ord_poly : ['a] ord = object
  inherit ['a] ord_base
  method compare x y   = of_comparison (Pervasives.compare x y)
  method less_equal    = Pervasives.(<=)
  method less_than     = Pervasives.(< )
  method greater_equal = Pervasives.(>=)
  method greater_than  = Pervasives.(> )
  method max           = Pervasives.max
  method min           = Pervasives.min
end

let ord_int    = (new ord_poly :> int    ord)
and ord_float  = (new ord_poly :> float  ord)
and ord_char   = (new ord_poly :> char   ord)
and ord_string = (new ord_poly :> string ord)

(Note the use of the injection into ordering). The case for pairs requires appropriate witnesses as before:

let ord_pair (l : 'a ord) (r : 'b ord) : ('a * 'b) ord = object
  inherit ['a * 'b] ord_base
  method equal = (eq_pair (l :> 'a eq) (r :> 'b eq))#equal
  method compare (p, q) (p', q') =
    match l#compare p p' with EQ -> r#compare q q' | c -> c
end

In this case, delegating equal requires passing the witnesses to eq_pair explicitly coerced to the eq class type. Finally, the classes for options and lists are straightforward applications of the encoding:

let ord_option (o : 'a ord) : 'a option ord = object
  inherit ['a option] ord_base
  method equal = (eq_option (o :> 'a eq))#equal
  method compare x y = match x with
    None   -> (match y with None -> EQ | Some _ -> LT)
  | Some x -> (match y with None -> GT | Some y -> o#compare x y)
end

let ord_list (o : 'a ord) : 'a list ord = object
  inherit ['a list] ord_base
  method equal = (eq_list (o :> 'a eq))#equal
  method compare =
    let rec compare x y = match x, y with
    | [], [] -> EQ
    | _ , [] -> GT
    | [], _  -> LT
    | x :: xs, y :: ys -> match o#compare x y with
    | EQ -> compare xs ys
    | c  -> c
    in compare
end

As it is clear, the encoding shows a direct correspondence between Haskell type classes and OCaml's classes and objects:

• type classes into class types with top-level functions dispatching on a witness object of that class type
• derived type classes into inheriting class types
• default implementations into virtual classes
• instances into objects inheriting from the default virtual class
• derived instances into objects having witnesses of the appropriate class type

In every case, the witness objects are used purely as closed vtables without state. It would be interesting to investigate which use cases would open using row polymorphism or data members. Also, note that there is no need to abstract over the object types, as each witness carries with it the intended implementation in a type-safe manner.

This technique is analogous to the one using functors to encode type classes, but then why have both in the same language?, in the words of Jacques Garrigue. One reason is that functors are not first-class values in OCaml but objects are, which makes using them as type witnesses much more lightweight. On the other hand, one limitation that functors don't have is that this encoding is limited to first-order type classes. In other words, it is not clear what would be required to implement Haskell type classes like:

instance  (Monad m) => Functor m  where
    fmap f x = bind x (return . f)

where m is a type constructor with sort * → * using the encoding presented here, whereas it is straightforward to concoct a (ML) functor:

module MonadFunctor (M : MONAD) : FUNCTOR = struct
  type 'a t = 'a M.t
  let fmap f x = M.bind x (fun v -> M.return (f v))
end

Another limitation is the need to pass a witness object to the type-indexed functions. One would ideally want to write something like:

let (===) (x : eq) = x#equal

where the value is its own witness, but obviously this would require that every value be wrapped into an object, requiring, for instance, code like the following:

if (new eq_int 5) === (new eq_int x) then …

Moreover, in order to actually operate on the wrapped values, the classes would need an explicit accessor. OCaml supports double dispatch making possible forcing the types of x and y to be equal:

class type ['a] eq = object ('self)
  method value     : 'a
  method equal     : 'self -> bool
  method not_equal : 'self -> bool
end

class eq_int x : [int] eq = object (self : 'self)
  method value                    = x
  method equal     (that : 'self) = self#value == that#value
  method not_equal (that : 'self) = self#value != that#value
end

Canonicalizing the witnesses for finite types like bool is very tedious:

let eq_bool : bool -> bool eq =
  let _t : bool eq = object
    method value          = true
    method equal     that =      that#value
    method not_equal that = not (that#value)
  end and _f : bool eq = object
    method value          = false
    method equal     that = not (that#value)
    method not_equal that =      that#value
  end in fun b -> if b then _t else _f

(essentially, a Church-encoded boolean). More importantly, this encoding is much more dynamic, making it rather remote with respect to the original, fully static Haskell semantics (this, incidentally, is a definite advantage of the functorial encoding).

In closing, it would be interesting to see how far this technique can be carried, especially to implement a numeric tower analogous to Haskell's, or maybe a better type class hierarchy to encode would be that of the Numeric Prelude. Another necessary avenue of investigation is measuring the abstraction penalty incurred by this encoding. In any case, I believe this is a neat showcase of the often-forgotten object-oriented features in OCaml.