The Coq mailing list

[Casteran Pierre <pierre.casteran AT labri.fr>]

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