The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Sun, 22 May 2011 17:41:50 +0200,
David Baelde 
<david.baelde AT gmail.com>
 a écrit :

> 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,

I also guess that if "'a" is a type which cardinality is quite small,
and you can extract [0,1] to float, then you can write a short ML code:

let dice_throw =
  let sieve = Random.float 1. in
  let rec get_rand acc l =
    match l with
    | v::l -> let acc = acc + μ v in
              if acc > sieve then v else get_rand acc l
    | [] -> failwith "Hmm, this is unexpected!"
  in get_rand 0 [list of all the elements of your type]

of course if you have big types for 'a such as int it can be too long
and even false due to rounding errors (the failwith case can even
occur).
You also have to identify the "μ" function (if it is the one I think
of, it is also called μ in Alea, so it should be extracted to its
Unicode code, as unicode is not supported by OCaml, leading to some
awfull identifier).
Even in this case, I am not sure it can be very usefull, but if it is,
then you won't have to rewrite all the ML code, and won't have to play
with the Extraction mechanism too much (and using P. Corbineau
solution seems also hazardous, as you change the extracted objects to
objects which are semantically very different; furthermore, using
side effects can mess a lot with extraction if some optimizations are
performed ("let x = side_effect () in let y = side_effect () in ..."
could be extracted to "let x = side_effect () in let y = x in ..." as
well as identity due to Coq semantics, but the two functions are
clearly different with OCaml)).