Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Free monads and strict positivity

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Free monads and strict positivity


Chronological Thread 
  • From: Pierre-Evariste Dagand <pierre-evariste.dagand AT ens-cachan.org>
  • To: coq-club AT inria.fr, johnw AT newartisans.com
  • Subject: Re: [Coq-Club] Free monads and strict positivity
  • Date: Mon, 6 Oct 2014 23:59:05 +0200

> Following an example of something
> Conor posted in Coq-club long ago, I've tried this:
>
> Inductive Kleene {I} (F : (I → Type) → I → Type) (p : I → Type) (i : I)
> :=
> | Ret : p i → Kleene F p i
> | Do : (forall q, F q i) → Kleene F p i.

Hmm, that's definitely not what you want.

For the sake of simplicity, let's take the non-indexed free monad. It
says: give me a functor F : Type -> Type, I will build a monad over
Type, ie. we are aiming for :

Free (F : Type -> Type)(V : Type) : Type

One possible intuition here is that you're building trees/terms whose
nodes are of F-shape and whose leaves are variables in V. The return
of your monad will be returning a variable in V:

return : V -> Free F V

while the bind will be the (simultaneous) substitution of a
V-variables by trees with W-variables:

bind : Free F V -> (V -> Free F W) -> Free F W

Well, the easiest way to define this is by building the following
(least) fixpoint (the "term algebra") :

Inductive Free (F : Type -> Type)(V : Type) : Type :=
| Ret : V -> Free F V (* leaves are variables *)
| Do : F (Free F V) -> Free F V (* nodes of F-shapes of terms *)

(Defining the bind is left as an exercise. Hint: you should probably
start implementing the join : Free F (Free F V) -> Free F V and apply
the usual Kleisli construction to get the bind)

Now, as you've noticed, Coq isn't too happy about the above definition
of Free: in the 'Do', 'Free F V' could appear negatively in 'F', at
which point the Gates of Hell usually open.

You need to tell Coq that you won't be using such a harmful functor.
The trick of the trade there is to use a "W-type". Since that's old
hat, let me give you the indexed version straightaway:

Record Signature (I : Type): Type
:= { Operations: I → Type;
Arities: forall i: I, Operations i → Type;
Sorts: forall i: I,
forall op: Operations i,
Arities i op → I }.
Arguments Operations [_] _ i.
Arguments Arities [_] _ [_] op.
Arguments Sorts [_] _ [_] [_] ar.

From these objects, you build functors:

Definition Functor {I} (S: Signature I)(X : I → Type)(i : I): Type
:= { op : Operations S i
& forall ar : Arities S op, X (Sorts S ar) }.

Note that this little guy is strictly-positive, by construction. So
you can use it to define the free monad, to Coq's great delight:

Inductive Kleene {I} (S: Signature I)(p : I → Type) (i : I) :=
| Ret : p i → Kleene S p i
| Do : Functor S (Kleene S p) i → Kleene S p i.


Now, to translate that paper, everywhere Conor is manipulating
functors, you should work on 'Signatures'. Implementing such system in
type theory is a Scottish cottage industry: you should many
implementations north of the Border (perhaps starting with Brady's
"Programming and Reasoning with Algebraic Effects and Dependent Types"
and then harassing Stevan Andjelkovic -- Conor's student -- to first
write and then publish his PhD thesis online).


Have fun,

--
Pierre



Archive powered by MHonArc 2.6.18.

Top of Page