Reasoning about distributions of random variables (how to do it?)

[Ilmārs Cīrulis]

https://www.reddit.com/r/Idris/comments/6eib1a/reasoning_about_distributions_of_random_variables/

Is some advanced variation of RND possible - that goes together with its distribution which could be reasoned about but is deleted before compilation?
(Kind of similar to the List Monad - it should be possible to reason about result of [x + y | x <- [1,2,..,n], y <- [1,2,..,m] ] etc.)

Reposting it here, too.

Maybe I should do it by myself (learn enough of Idris, then tinker until its working), but, realistically, I have no time for that. :(

 

[Guillaume Andrieu]

Hi Ilmars.

Probability monads are quite a thing, well studied since a long time.

Here is a library that does this in Scala:
    https://github.com/jliszka/probability-monad
This is how you do it in Haskell:
    http://www.randomhacks.net/files/build-your-own-probability-monads.pdf

And this is the library that does it in Idris !
    https://github.com/blackbrane/probability

Cheers!
Guillaume.

[Ilmārs Cīrulis]

Hello, Guillaume.
 
Yes, as a monad it is not complex (kind of similar to standard List Monad). I could make my own or use some already existing one.

 

But what I want is already existing RND (which is effect and those I don't understand yet) but with probability distribution which can be reasoned about. This "RND2" would work as standard RND when compiled - like a call of some random() function.

Cheers too,

Ilmars