ITrees

The Free monad:

Recall the definition of FFree:
Inductive FFree (E : Type → Type) (R : Type) : Type :=
| Ret (x : R)
| Do {X} (op : E X) (k : X → FFree E R).

A Coinductive Version of FFree

  CoInductive itree (E : Type → Type) (R : Type) :=
  | Ret (r:R)
  | Tau (t : itree E R)
  | Vis {X:Type} (e: E X) (k : X → itree E R).

Represents computations that can:

Terminate by returning a value of type R
Perform an internal step of computation, before continuing to compute
Trigger an event e expecting a certain answer of type X. It then continues to compute, but must be ready to do so no matter what is the environment's answer: it therefore takes a continuation indexed by X

(ASIDE) The "real" Interaction Trees data-structure

In practice, we use a slightly different definition, where the type itree is defined as the final coalgebra ("greatest fixed point") of the functor itreeF:

Our two parameters, domain of events and return type

Context {E : Type → Type} {R : Type}.

  Variant itreeF (itree : Type) :=
    | RetF (r : R)
    | TauF (t : itree)
    | VisF {X : Type} (e : E X) (k : X → itree)
  .

Note: this is a coinductive definition

CoInductive itree : Type := go
{ _observe : itreeF itree }.

And we introduce some notation to make it look like the previous definition.

First examples of itree computations

We first define the Input/Output events informally described above

  Variant IOE : Type → Type :=
    | Output (n : nat) : IOE unit
    | Input : IOE nat.

Here is a very boring computation that simply returns 1789

Definition aux_armes : itree IOE nat := Ret 1789.

And one that requests a value from the user and doubles it

Definition double : itree IOE nat :=
Vis Input (fun n ⇒ Ret (2 × n)).

A program that repeatedly does I/O:

CoFixpoint echo : itree IOE void :=
Vis Input (fun n ⇒ Vis (Output n) (fun _ ⇒ echo)).

Silent Divergence

And finally, an important: the silently diverging computation

CoFixpoint spin_spec : itree IOE void :=
Tau spin_spec.

spin can have any type at all.

CoFixpoint spin {E R} : itree E R := Tau spin.

Failure

Consider now an event whose return type is empty

Variant Empty : Type → Type :=
| empty : Empty void.

The environment cannot respond to this event

Definition fail {R} : itree Empty R :=
Vis empty (fun x : void ⇒ match x with end).

Substitution:

As with the FFree monad, we can define a "substitution" operation, which looks for all the Ret x leaves of the tree and applies a continuation k to build a bigger tree :

  Definition subst {E : Type → Type} {T U : Type} (k : T → itree E U)
  : itree E T → itree E U :=
    cofix _subst (u : itree E T) : itree E U :=
    match u with
    | Ret r ⇒ k r
    | Tau t ⇒ Tau (_subst t)
    | Vis e h ⇒ Vis e (fun x ⇒ _subst (h x))
    end.

Monad operations

These ingredients give us all we need to define a monad.

Return is just Ret

Bind is just subst with the arguments reordered:

Definition bind {E : Type → Type} {T U : Type} (u : itree E T) (k : T → itree E U)
: itree E U := subst k u.

An elementary itree computation emits an event:

Definition trigger {E : Type → Type} {A : Type} (e : E A) : itree E A :=
Vis e (fun x ⇒ Ret x).

Iteration

What about loops?

Definition iter {E : Type → Type} {R I: Type}
           (step : I → itree E (I + R)) : I → itree E R :=
  cofix iter_ i :=
    lr <- step i;; (* one step of the loop *)
    match lr with
    | inl l ⇒ Tau (iter_ l) (* got a new acc. => jump back into loop *)
    | inr r ⇒ Ret r (* got a final result => terminate *)
    end.

Note: the backwards jump is guarded by Tau

Example:

Define the factorial fact n using the iter combinator.

Definition fact (n : nat) : itree voidE nat :=
iter (fun '(acc,n) ⇒
          match n with
          | O ⇒ Ret (inr acc)
          | S m ⇒ Ret (inl (n × acc, m))
end) (1,n).

"Running" an itrees computation

We cannot simply use Eval compute in ... to "run" an itree computation. But, we can provide "fuel" that can be burned to force it:

Fixpoint burn (n : nat) {E R} (t : itree E R) :=
  match n with
  | O ⇒ t
  | S n ⇒
    match observe t with
    | RetF r ⇒ Ret r
    | VisF e k ⇒ Vis e k
    | TauF t' ⇒ burn n t'
    end
  end.

You can this way test that your factorial computes what it should

Eval compute in burn 10 (fact 6).

==> Ret 720 : itree voidE nat

A useful specialization for Imp Semantics

Imperative loops are particular patterns of recursion: they do not carry any notion of accumulator. We can capture this pattern with a repeat combinator.

Definition repeat {E} (step : itree E (unit + unit)) : itree E unit :=
iter (fun _ ⇒ step) tt.

Mutual recursion

The coq development also shows how to encode full, mutual, general-recursive operations.

But we'll skip it here, since we don't need that for Imp.