How do you prove probabilities are closed under multiplication with dependent types?

Question

I'm working a bit with Idris and I've written a type for probabilities - Floats between 0.0 and 1.0:

data Probability : Type where
    MkProbability : (x : Float) -> ((x >= 0.0) && (x <= 1.0) = True) -> Probability

I want to be able to multiply them:

multProbability : Probability -> Probability -> Probability
multProbability (MkProbability p1 proof1) (MkProbability p2 proof2) =
    MkProbability (p1 * p2) ???

How can I prove that p1 * p2 will always be a probability?

Answer 1

I'd remove floating-point numbers from the picture. You're almost always going to have problems with primitives, but especially when dealing with the weird details of the IEEE 754 type.

Instead, I'd represent probabilities using a ratio type:

record Probability : Type where
  MkProbability : (numerator : Nat) ->
                  (denominator : Nat) ->
                  LTE numerator (S denominator) ->
                  Probability

LTE is a type where values only exist when the first Nat is less than or equal to the second Nat. The (S denominator) is to ensure we don't have a denominator of zero. This means MkProbability 2 1 (LTESucc LTEZero) is valid and represents a probability 1.0, looks weird but ensures validity.

We can then get a Float out of the type:

toFloat : Probability -> Float
toFloat (MkProbability n d _) =
  fromInteger (toIntegerNat n) / fromInteger (toIntegerNat (S d))

Another benefit is that this is arbitrary precision until we convert to a Float.

A problem is that you're probably going to have to build large LTE values. Using isLTE for runtime values will probably help here!