The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Below is a very generic approach to the free-monad thing. It is parametrized by the commands you may want to execute in your monad (in fact the free monad construction is a sort of W-type with an extra constructor for returns). An interesting side-effect of this generic definition, is that the (dependent) recursor of the free monad corresponds exactly to the type of handlers in the algebraic effect language Eff ( http://math.andrej.com/eff/ ).

Record Signature := {
  Command: Type;
  RType: Command -> Type
}.

Section FreeMonad.

  Variable (S:Signature).

  Inductive Free (A:Type) : Type :=
  | return_ (a:A) : Free A
  | run (c:S.(Command)) (k:S.(RType) c -> Free A) : Free A
  .
  Arguments return_ {A} a.
  Arguments run {A} c k.

  Fixpoint bind {A B:Type} (x:Free A) (f:A->Free B) : Free B :=
    match x with
    | return_ a => f a
    | run c k => run c (fun r => bind (k r) f)
    end
  .

  Definition join {A:Type} (x:Free (Free A)) : Free A :=
    bind x (fun a => a)
  .

  Check (fun n : Free (Free nat) => join  n): Free (Free nat) -> Free nat.

End FreeMonad.

On 24 June 2013 11:00, Casteran Pierre <pierre.casteran AT labri.fr> wrote:

Thanks, Cédric and Arnaud,

It may not work in general, but in this particular case, the definition
of the free monad over Random is:

Inductive MM (B:Type):  Type :=
   MM_Return (b:B)
| MM_Random (n:nat)(f : nat -> MM B) .

MM_Bind can be defined by recursion. And I think (not tested) that join
will work as expected.

I have some difficulty in defining MM_Bind by recursion:
In my development, I have three interpretations of any term of type
MM B : as a set (of type Ensemble B), as a distribution (using ALEA library), or as a function driven by a pseudo-random generator (for testing).

Then, I write  algorithms that contains calls to random expressions as terms of type MM B : such programs contain a lot of calls to Bind with
various return types : booleans, integers, sets, states, etc.
The three semantics above are useful for reasoning about programs, and
I think it's important to maintain a unique free object as a source of
various semantics.

I'll try to find some solution, or check whether join is really useful
in this context. At this time I just tried it for the fun, without any necessity.

The best,

Pierre