Free

Extensible Semantics and the Free Monad

OPLSS synergy with algebraic effects and handlers.

A toy expression language AST

Inductive Expr : Set :=
| Val (n : nat)
| Add (e1 e2 : Expr).
Its evaluation function:
Fixpoint eval (e : Expr) : nat :=
  match e with
  | Val n ⇒ n
  | Add e1 e2 ⇒ eval e1 + eval e2
  end.
Example e : Expr := Add (Val 3) (Val 4).
Eval compute in eval e.
==> 7 : nat

The expression problem

Consider adding a new operation:
Inductive Expr' : Set :=
| Val' (n : nat)
| Add' (e1 e2 : Expr')
| Minus' (e1 e2 : Expr').
Fixpoint eval' (e : Expr') : nat :=
  match e with
  | Val' n ⇒ n
  | Add' e1 e2 ⇒ eval' e1 + eval' e2
  | Minus' e1 e2 ⇒ eval' e1 - eval' e2
  end.
Example e' : Expr' := Minus' (Val' 7) (Val' 4).
Eval compute in eval' e'.
==> 3 : nat
This works, but isn't very extensible.

One solution (Datatypes à la carte)

Add a parameter so Expr Op is now either
  • a value, or,
  • a computation that first performs an Op, and then builds a new expression indexed by a natural number.
In the latter case, we think of the index provided to continuation k as the result of computing op.
M : X -> Free Op X pure/ret : X -> Free Op X bind/seq : Free Op X -> (X -> Free Op Y) -> Free Op Y
Free F := F (Free F)
Inductive Expr (Op : Type) :=
| Val (n : nat)
| Do (op : Op) (k : nat → Expr Op).

Instantiating Op

Now define Plus like this, which extends the syntax of Expr:
Inductive Plus := add (n1 n2 : nat).
It looks a bit weird, but we can write the Expr summing 3 and 4 and returning the result as follows:
Example e : Expr Plus := Do (add 3 4) (fun n ⇒ Val n).

A naive interpreter

The next thing we wanted to do is to define an evaluation function. We could do it directly:
Fixpoint eval_naive (t : Expr Plus) : nat :=
  match t with
  | Val n ⇒ n
  | Do (add n m) k ⇒ eval_naive (k (n + m))
  end.
Eval compute in (eval_naive e).
==> 7 : nat
But if we did that, we would have a weirder syntax, and gained nothing.

A better way:

Parameterize the evaluator by a handler h.
Fixpoint fold_eval {Op} (h : Op → nat) (t : Expr Op) : nat :=
  match t with
  | Val n ⇒ n
  | Do op k ⇒ fold_eval h (k (h op))
  end.
A handler for Plus:
Definition hplus : Plus → nat :=
        fun '(add n1 n2) ⇒ n1 + n2.
Definition evalp := fold_eval hplus.
Eval compute in evalp e.
==> 7 : nat

Sequential composition

Fixpoint seq {Op} (e : Expr Op) (k : nat → Expr Op) : Expr Op :=
  match e with
  | Val n ⇒ k n
  | Do op h ⇒ Do op (fun n ⇒ seq (h n) k)
  end.
Notation "x <- t1 ;; t2" := (seq t1 (fun x ⇒ t2))
(Not quite a monad yet, it is too specific.)

Operations as "triggerable" events.

trigger op does op and returns its value.
Definition trigger {Op} (op : Op): Expr Op :=
  Do op (fun x ⇒ Val x).

With this, we can already write examples a bit more comfortably:
Example e1 : Expr Plus :=
  trigger (add 3 4).
Eval compute in evalp e1.
==> 7 : nat

Example e2 : Expr Plus :=
        x <- trigger (add 1 2);;
        y <- trigger (add 3 4);;
        trigger (add x y).
Eval compute in evalp e2.
==> 10 : nat

Adding another operation

Inductive Minus := sub (n1 n2 : nat).
A handler for Minus:
Definition hminus : Minus → nat :=
  fun '(sub n1 n2) ⇒ n1 - n2.
used for evaluation
Definition evalm := fold_eval hminus.

Example e3 : Expr Minus :=
  trigger (sub 4 3).
Eval compute in evalm e3.
==> 1 : nat

Example e4 : Expr Minus :=
        x <- trigger (sub 2 1);;
        y <- trigger (sub 6 3);;
        trigger (sub y x).
Eval compute in evalm e4.
==> 2 : nat

Supporting Multiple Operations

Define the disjoint sum of operations:
Notation "Op1 +' Op2" := ((Op1 + Op2)%type) (at level 10).
An expression of type Expr (Plus +' Minus) can perform both operations
Furthermore, we can combine two handlers generically:
Definition hsum {Op1 Op2} (h1 : Op1 → nat) (h2 : Op2 → nat)
        : Op1 +' Op2 → nat :=
        fun op ⇒ match op with
        | inl op ⇒ h1 op
        | inr op ⇒ h2 op
        end.
Notation "h1 ⊕ h2" := (hsum h1 h2) (at level 10).

Example evaluation:

We hence can evaluate mixed expressions as well without any additional definitions
Definition eval := fold_eval (hplus ⊕ hminus).
Example e5 : Expr (Plus +' Minus) :=
        x <- trigger (inr (sub 2 1));;
        y <- trigger (inr (sub 6 3));;
        trigger (inl (add x y)).
Eval compute in eval e5.
==> 4 : nat

Using explicit inl and inr is painful, so...

Introduce a typeclass of injections:
Class Subop Op1 Op2 := inject : Op1 → Op2.
#[local] Instance subop_refl Op : Subop Op Op :=
  fun x ⇒ x.
#[local] Instance subop_left Op1 Op2 :
  Subop Op1 (Op1 +' Op2) := inl.
#[local] Instance subop_right Op1 Op2 Op3 `{Subop Op1 Op3}
  : Subop Op1 (Op2 +' Op3)
  := fun e ⇒ inr (inject e).
Notation trigger' e := (trigger (inject e)).

Now trigger' hides inl and inr:

Example e5' : Expr (Plus +' Minus) :=
        x <- trigger' (sub 2 1);;
        y <- trigger' (sub 6 3);;
        trigger' (add x y).
Eval compute in (eval e5').
==> 4 : nat

More syntactic sugar

Notation add' n m := (trigger' (add n m)).
Notation sub' n m := (trigger' (sub n m)).
Example e5'' : Expr (Plus +' Minus) :=
        x <- sub' 2 1;;
        y <- sub' 6 3;;
        add' x y.
Eval compute in eval e5''.
==> 4 : nat

Expr Op as a semantics

Note that, instead of seeing Expr Op as our programming language itself, we can see it alternatively as a semantic domain for our original syntax.
Inductive ExprAST : Set :=
| ValAST (n : nat)
| AddAST (e1 e2 : ExprAST)
| MinusAST (e1 e2 : ExprAST).
Fixpoint repr (e : ExprAST) : Expr (Plus +' Minus) :=
  match e with
  | ValAST n ⇒ Val n
  | AddAST e1 e2 ⇒
      x <- repr e1;;
      y <- repr e2;;
      add' x y
  | MinusAST e1 e2 ⇒
      x <- repr e1;;
      y <- repr e2;;
      sub' x y
  end.
Definition sem (e : ExprAST) : nat := eval (repr e).

Example e6 : ExprAST :=
  MinusAST (AddAST (ValAST 3) (ValAST 4)) (ValAST 5).
Eval compute in (sem e6).
==> 2 : nat

Free Monads

Expr Op was specific to nat operators and nat computations. We can make it more generic:
Inductive FFree (E : Type → Type) (R : Type) : Type :=
| Ret (x : R)
| Do {X} (op : E X) (k : X → FFree E R).
Note that op is now characterized by an indexed type E, and op : E X means that, semantically, op produces an X (which will be fed to the continuation k).

Operations, dependently

In this format, the signature of the addition operation looks like the following:
Inductive Plus : Type → Type :=
  add (n1 n2 : nat) : Plus nat.
Or, for Boolean operations:
Inductive BoolOp : Type → Type :=
| or (b1 b2 : bool) : BoolOp bool
| not (b : bool) : BoolOp bool.

Handling operations

The implementation of an operation is now aware of the type it must implement.
Definition hplus : ∀ X, Plus X → X :=
        fun _ '(add n1 n2) ⇒ n1 + n2.
Definition hbool : ∀ X, BoolOp X → X :=
        fun _ op ⇒ match op with
        | or b1 b2 ⇒ orb b1 b2
        | not b ⇒ negb b
        end.

fold_pure, generically

We can now write a "fold" operation that computes a result of type R
Fixpoint fold_pure {E R} (h : ∀ X, E X → X) (t : FFree E R) : R :=
  match t with
  | Ret x ⇒ x
  | Do op k ⇒ fold_pure h (k (h _ op))
  end.

Sequential composition

We can rebuild the machinery from before, but this time seq is the bind of a monad FFree E.
Fixpoint seq {E X Y} (e : FFree E X) (k : X → FFree E Y) : FFree E Y :=
  match e with
  | Ret x ⇒ k x
  | Do op h ⇒ Do op (fun n ⇒ seq (h n) k)
  end.
#[export] Instance FFreeM {E} : Monad (FFree E) :=
{|
    ret := @Ret E
  ; bind := @seq E
|}.

Equivalence of FFree E computations

We define an appropriate notion of equivalence.
Note that the continuations are required to be extensionally equivalent.
Inductive eq_FFree {E X} : FFree E X → FFree E X → Prop :=
| eq_Ret : ∀ (x:X), eq_FFree (Ret x) (Ret x)
| eq_Do : ∀ {Y} (op : E Y) (k1 k2 : Y → FFree E X)
             (Heq: ∀ (y1 y2:Y), y1 = y2 → eq_FFree (k1 y1) (k2 y2)),
    eq_FFree (Do op k1) (Do op k2).
Use straightforward induction to prove that eq_FFree is an equivalence relation.
#[local] Instance eqM_FFree {E} : EqM (FFree E) :=
  fun A ⇒ (@eq_FFree E A).
#[local] Instance eqM_FFree_Equiv {E} : EqMEquivalence (FFree E).
Proof.
  constructor; typeclasses eauto.
Qed.

Monad Laws for FFree E :

Next we prove the monad laws, but they follow straightforwardly by induction:
#[local] Instance eqm_FFree_monad_laws {E} : MonadLaws (FFree E).
Proof.
  constructor.
  - intros A B C ma.
    induction ma; intros; simpl in ×.
    + reflexivity.
    + constructor. intros. rewrite H.
      subst.
      reflexivity.
  - intros A B C ma.
    reflexivity.
  - intros.
    induction m; intros; simpl in ×.
    + reflexivity.
    + constructor. intros. subst. rewrite H. reflexivity.
  - repeat red. intros A B x.
    induction x; intros y Heq k1 k2 HK.
    + inversion Heq. subst.
      simpl. apply HK.
    + inversion Heq. subst.
    apply inj_pair2 in H2. subst.
    apply inj_pair2 in H3. subst.
    simpl.
    constructor.
    intros. subst.
    apply H. apply Heq0.
    simpl. reflexivity.
    assumption.
Qed.

Disjoint sum of Indexed Types

Now that our operation types are indexed by their return types, we need to provide an appropriate notion of "disjoint union":
Inductive sumi (E1 E2 : Type → Type) (X : Type) : Type :=
        | inli (_ : E1 X)
        | inri (_ : E2 X).
Notation "Op1 +' Op2" := (sumi Op1 Op2) (at level 10).
We can also "sum" handlers:
Definition hpure_sum {Op1 Op2} (h1 : ∀ X, Op1 X → X) (h2 : ∀ X, Op2 X → X)
        : ∀ X, (Op1 +' Op2) X → X :=
        fun _ op ⇒ match op with
        | inli op ⇒ h1 _ op
        | inri op ⇒ h2 _ op
        end.

Implicit injections

And, using similar typeclass machinery to what we saw previously, use inference to inject an op : E X into, e.g., a sum (E +' F) X.
Which allows us to define a generic trigger operation:
Definition trigger_ {E X} (e : E X) :=
        Do e (fun x ⇒ Ret x).
Notation trigger e := (trigger_ (inject e)).

Putting it all together:

Example e1 : FFree (Plus +' BoolOp) nat :=
  b <- trigger (or true false);;
  if (b : bool)
  then trigger (add 10 10)
  else trigger (add 2 2).
Eval compute in fold_pure (hpure_sum hplus hbool) e1.
==> 20 : nat

Recap:

  • Use the FFree E monad to define computations parameterized by "syntax" for operations like Plus.
  • Define the semantics of those operations separately using handlers
  • Use fold_pure as an interpreter to evaluate the handlers
Aside: Technically, FFree E is a freer monad, not the "Free" monad.

Impure Interpretations

Now consider supporting impure operations.
Inductive Cell : Type → Type :=
| Rd : Cell nat
| Wr (n : nat) : Cell unit.
There is no problem using FFree Cell (the operations have no semantics):
Example double : FFree (Plus +' Cell) unit :=
  x <- trigger Rd;;
  xx <- trigger (add x x);;
  trigger (Wr xx).

Monadic fold, or Monadic Interpreters

First: some handy notation for "polymorphic" functions:
Notation "E ~> F" := (∀ X, E X → F X) (at level 30).
We can now redefine our folding function over monadic implementations of our effects
Fixpoint fold {E M} `{Monad M} (h : E ~> M) [R] (t : FFree E R) : M R :=
  match t with
  | Ret x ⇒ ret x
  | Do op k ⇒ x <- h _ op;; fold h (k x)
  end.

A handler can now be monadic

The type of this handler returns a computation in the state monad:
Definition hcell : Cell ~> state nat :=
  fun _ e ⇒
    match e with
    | Wr n ⇒ put n
    | Rd ⇒ get
    end.
Intuitively, this means that we can interpret the operations Wr and Rd by their semantic counterpart.

Lifting computations

We do have to lift the pure handler hplus into the state monad.
With a bit more help from typeclasses, we could do it automatically.
Definition hplusS : Plus ~> state nat :=
  fun _ e ⇒ ret (hplus _ e).

Running the example

Recalling our example from earlier:
Example double : FFree (Plus +' Cell) unit :=
  x <- trigger Rd;;
  xx <- trigger (add x x);;
  trigger (Wr xx).
We can now run it in the state monad:
Eval compute in fold (hplusS ⊕ hcell) double 16.
==> (32, tt) : nat × unit
Eval compute in (fold (hplusS ⊕ hcell) (double ;; trigger Rd) 42).
==> (84, 84) : nat × unit

Next: ITrees

At this point, are we ready to tackle ITrees