Require Import ssreflect ssrnat.
Set Implicit Arguments.
Set Contextual Implicit.
Set Maximal Implicit Insertion.
(** * Free monads in the abstract: *)
(* Think in terms of algebraic theory: a free monad is the free term
algebra of a signature. For simplicity, I will code signature as
follows: *)
Record Signature: Type :=
MkSig { Ops : Type ;
Ar : Ops -> Type }.
(* Therefore, the term algebra will be either a variable over some set
X or a compound term: *)
Inductive Free (Σ: Signature)(X: Type): Type :=
| var (x: X): Free Σ X
| term (op: Ops Σ)(rec: Ar Σ op -> Free Σ X): Free Σ X.
Arguments var [Σ X] x.
Arguments term [Σ X] op rec.
(** ** Example: Binary tree *)
(* This example is taken from "Asymptotic Improvement of Computations
over Free Monads", Voigtländer. It is just to give you some
intuition for signatures. *)
Section Example.
Definition ΣTree: Signature := @MkSig unit (fun _ => bool).
Definition Tree (X: Type) := Free ΣTree X.
Definition leaf {X: Type}(x: X): Tree X := var x.
Definition node {X: Type}(l r: Tree X): Tree X :=
@term ΣTree _ tt (fun b => if b then l else r).
End Example.
(** * Free monad "in the concrete" *)
(* It is rather unpleasant to deal with the general case and it
wouldn't exhibit the performance issues I'm interested in. So I'll
develop my presentation on the hard-coded free monad of trees: *)
Inductive FreeTree (X: Type): Type :=
| var' (x: X): FreeTree X
| node' (l r: FreeTree X): FreeTree X.
Notation "'leaf''" := (var').
Arguments var' [X] x.
Arguments node' [X] l r.
(* Modulo extensionality, you can generalize the definitions and
results in this file with s/FreeTree/Free Σ/. We could get rid of
extensionality by giving a more intensional definition of
signatures. *)
(** ** Monadic operations *)
(* Reassuringly, we can implement the usual monadic operations. Note
that 'bind' corresponds to variable substitution. Since there is no
notion of binding, there is no need for renaming, etc. *)
Section MonadOps.
Variables (X Y: Type).
Definition ret (x: X): FreeTree X := var' x.
Fixpoint bind (mx: FreeTree X)(f: X -> FreeTree Y): FreeTree Y :=
match mx with
| var' x => f x
| node' l r => node' (bind l f) (bind r f)
end.
End MonadOps.
(** ** Monad laws *)
(* Well, they hold. *)
Section MonadLaws.
Variables (X Y Z: Type).
Lemma bind_left_unit:
forall (x: X)(f: X -> FreeTree Y),
bind (ret x) f = f x.
Proof.
move=> x f //=.
Qed.
Lemma bind_right_unit:
forall (mx: FreeTree X),
bind mx ret = mx.
Proof.
elim=> [x | l ? r ?] //=.
(* Case: mx ~ term op rec *)
apply f_equal2; assumption.
Qed.
Lemma bind_compose:
forall (mx: FreeTree X)(f: X -> FreeTree Y)(g: Y -> FreeTree Z),
bind (bind mx f) g = bind mx (fun a => bind (f a) g).
Proof.
case=> [x | l r f g] //=.
(* Case: mx ~ term op rec *)
apply f_equal2.
(* Case: left branch *)
elim: l => [|ll ? rl ?] //=;
apply f_equal2; assumption.
(* Case: right branch *)
elim: r => [|lr ? rr ?] //=;
apply f_equal2; assumption.
Qed.
End MonadLaws.
(** ** Example: monadic programming *)
Section FullTree.
(* We can build a fancy tree in this monad.
Complexity: O(2ⁱ) *)
Fixpoint fullTree (i: nat): FreeTree nat :=
match i with
| 0 => var' 0
| n.+1 => bind (fullTree n)
(fun i => node' (leaf' (n - i))
(leaf' (i.+1)))
end.
(* Then, we can, say, walk down such tree
Complexity: O(i) for a tree of depth i *)
Fixpoint zig (t: FreeTree nat) {struct t}: nat :=
match t with
| var' n => n
| node' l r => zag r
end
with zag (t: FreeTree nat) {struct t}: nat :=
match t with
| var' n => n
| node' l r => zig l
end.
Definition zigzag (t: FreeTree nat): nat := zig t.
(* As explained by Voigt, 'zigzag' has a quadratic execution time
(in cbn): at each node, we must force the 'bind'. *)
Time Eval lazy in (zigzag (fullTree 10)).
(* = 4 : nat
Finished transaction in 0. secs (0.u,0.s) *)
Time Eval lazy in (zigzag (fullTree 500)).
(* = 250 : nat
Finished transaction in 1. secs (0.732u,0.s) *)
Time Eval lazy in (zigzag (fullTree 1000)).
(* = 500 : nat
Finished transaction in 3. secs (2.76u,0.s) *)
Time Eval lazy in (zigzag (fullTree 1500)).
(* = 750 : nat
Finished transaction in 7. secs (6.164u,0.s) *)
Time Eval lazy in (zigzag (fullTree 2000)).
(* = 1000 : nat
Finished transaction in 11. secs (11.128u,0.s) *)
(* The crux of the matter is that while
bind (bind mx f) g = bind mx (fun a => bind (f a) g)
the complexity of both sides is not equivalent. The right-hand
side performs a single pass down the tree, while the left-hand
side will perform two passes: one for the inner bind and another
for the outer bind. Obviously, 'fullTree' has been crafted to
maximize such inefficient interleaving. *)
End FullTree.
(** * Going to Church *)
(* Inspired by Edward Kmett
[http://comonad.com/reader/2011/free-monads-for-less-2/], we switch to
an isomorphic but more efficient representation: the Church encoding!
*)
(* Recall (from Girard) that we can encode any inductive type through
an impredicative encoding:
μ F ≅ ∀ K. (F X → X) → F X
*)
(* Playing that trick on FreeTree, we get:
FreeTree X ≅ ∀ K. (X -> K) -> (K -> K -> K) -> K
*)
Definition FreeTree' (X: Type): Type
:= forall K,
(X -> K) ->
(K -> K -> K) -> K.
Definition leaf'' {X} (x: X): FreeTree' X :=
fun K kRet kBind => kRet x.
Definition node'' {X} (l r: FreeTree' X): FreeTree' X :=
fun K kRet kBind => kBind (l K kRet kBind) (r K kRet kBind).
(** ** Monadic operations *)
(* Business as usual here. *)
Section ChurchOps.
Variables (X Y: Type).
Definition ret' (x: X): FreeTree' X :=
fun K kRet kBind => kRet x.
Definition bind' (mx: FreeTree' X)(f: X -> FreeTree' Y): FreeTree' Y :=
fun K kRet kBind => mx K (fun x => f x K kRet kBind) kBind.
End ChurchOps.
Arguments ret' [X] x [K] kRet kBind.
Arguments bind' [X Y] mx f [K] kRet kBind.
(* We can reify the Church-encoded version into the inductive one, by
abusing initiality: *)
Definition run {X} (mx: FreeTree' X): FreeTree X := mx (FreeTree X) (@var' _) (@node' _).
(* The word 'reify' is not a coincidence here: if you're thinking in
terms of NbE, 'FreeTree'' is our semantic world, where 'FreeTree' is
quotiented by the equational theory of (free) monads. *)
(** ** Monad laws: *)
(* Interestingly, the laws now hold definitionally. Hum, very
interesting. *)
Section ChurchLaws.
Variables (X Y Z: Type).
Lemma bind_left_unit':
forall (x: X)(f: X -> FreeTree' Y),
bind' (ret' x) f = f x.
Proof.
move=> x f //=.
Qed.
Lemma bind_right_unit':
forall (mx: FreeTree' X),
bind' mx (@ret' X) = mx.
Proof.
move=> mx //=.
Qed.
Lemma bind_compose':
forall (mx: FreeTree' X)(f: X -> FreeTree' Y)(g: Y -> FreeTree' Z),
bind' (bind' mx f) g = bind' mx (fun a => bind' (f a) g).
Proof.
move=> mx f g //=.
(* ie., there is *definitionally* no difference between
left-nested or right-nested binds *)
Qed.
(* Booyah! *)
End ChurchLaws.
(** ** Example: Monadic programming (contd.) *)
Section ExampleChurch.
(* We rewrite fullTree in over our new monad/datatype of trees: *)
Fixpoint fullTree' (i: nat): FreeTree' nat :=
match i with
| 0 => @leaf'' _ 0
| n.+1 => bind'
(@fullTree' n)
(fun i => @node'' _ (@leaf'' _ (n - i))
(@leaf'' _ (i.+1)))
end.
(* To run 'zigzag', we can now compose the 'run' function – that
turns a Church-encoded tree into an actual tree – and fullTree'
above. And it goes way faster! *)
Time Eval lazy in (zigzag (run (@fullTree' 10))).
(* = 4 : nat
Finished transaction in 0. secs (0.u,0.s) *)
Time Eval lazy in (zigzag (run (@fullTree' 500))).
(* = 250 : nat
Finished transaction in 0. secs (0.08u,0.s) *)
Time Eval lazy in (zigzag (run (@fullTree' 1000))).
(* = 500 : nat
Finished transaction in 0. secs (0.26u,0.s) *)
Time Eval lazy in (zigzag (run (@fullTree' 1500))).
(* = 750 : nat
Finished transaction in 0. secs (0.608u,0.s) *)
Time Eval lazy in (zigzag (run (@fullTree' 2000))).
(* = 1000 : nat
Finished transaction in 1. secs (1.024u,0.s) *)
(* Why is it going faster? We had too many left-nested binds: the
Church-encoded representation normalizes (as in NbE) everyone to a
right-nested form. *)
End ExampleChurch.