Как вы доказываете, что вероятности замыкаются при умножении на зависимые типы?

Question

Я работаю немного с Идрисом и я написал тип вероятностей - Float сек между 0.0 и 1.0:

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

Я хочу, чтобы иметь возможность умножать:

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

Как я могу доказать, что p1 * p2 всегда будет вероятностью?

Answer 1

Я бы удалил числа с плавающей запятой из картинки. У вас почти всегда будут проблемы с примитивами, но особенно при работе со странными деталями типа IEEE 754.

Вместо этого, я бы представляют вероятности, используя тип отношения:

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

LTE представляет собой тип, где значения существуют только тогда, когда первый Nat меньше или равен второму Nat. (S denominator) должен гарантировать, что у нас нет знаменателя нуля. Это означает, что MkProbability 2 1 (LTESucc LTEZero) действителен и представляет вероятность 1.0, выглядит странно, но обеспечивает достоверность.

Мы можем затем получить Float из типа:

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

Другим преимуществом является то, что это с произвольной точностью, пока мы не преобразовать в Float.

Проблема в том, что вам, вероятно, придется строить большие значения LTE. Использование isLTE для значений времени выполнения, вероятно, поможет здесь!