The Coq mailing list

[Pierre-Evariste Dagand <pierre-evariste.dagand AT ens-cachan.org>]

> 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