does anyone have a favorite way to computationally formalize (basic) probability theory, in any language? features i'd want include:
- computing with the real unit interval as a type
- making sure distributions over possible values of a variable sum to 1, statically
- nice compositional ways to construct distributions, events, random variables
i'm wondering if, say, complete lattices in cubical agda are overkill for this task