The Coq mailing list

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

Hi,

 Talking about Free monads, let me quote two messages by Arnaud Spiwack 
in this list (messages posted on June 24th 2013: look at the archive)

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/ ).


In the messages  you can find the generic definition, then an 
instantiation to the monad generated by a command that calls a random 
generator.

Pierre