The Coq mailing list

[David Baelde <david.baelde AT gmail.com>]

Hi Allyx,

If you haven't already, you should have a look at the paper by
Audebaud & Paulin (http://dx.doi.org/10.1016/j.scico.2007.09.002)
about the ALEA library. It starts with a gentle introduction to the
monad that is used, detailing its advantages and drawbacks.

There are mainly two ways of representing probabilistic algorithms. A
computation returning objects of type 'a can be represented either as
(unit -> 'a) or ('a -> [0,1]). The first approach is suitable for
simulations: it gives you a function that you can re-run as many times
as you wish, possibly getting different results each time, because the
function relies on some random generator. The second approach, used in
ALEA, models the computation as a probability distribution. It is an
exact approach: for a given x of type 'a it should return the
probability that this x is obtained. But this will be unusable for
testing.

Long story short, Pierre Corbineau's solution will work. However, I
wouldn't bother to make extraction work for such small examples: just
rewrite the code in ML yourself.

Have fun,
-- 
David