Идрис: арифметика для ограниченного двойника

Здесь есть две проблемы. Double арифметика определяется с помощью примитива функций. Идрис не может даже доказать, что a <= b = True -> b <= c = True -> a <= c = True (что, кстати, даже не выполняется постоянно - так что это не вина Идриса). Нет никаких доказательств для a <= b = True, кроме как просто проверить это, то, что вы пробовали с ifThenElse.

При работе с такими слепыми доказательствами во время выполнения (так что просто … = True) _ 6_ весьма полезен. ifThenElse (a <= x) … … разветвляется при логической проверке, но код в ветвях не знает о результате проверки. С choose (a <= x) вы получите результат для ветвей, с Left prf и prf : So (a <= x) или Right prf и prf : So (not (a <= x)).

Я полагаю, если результат добавления двух ограниченных двойников будет больше, чем верхняя граница, результатом должна быть эта верхняя граница. Сделаем первую попытку:

import Data.So

data BoundedDouble : (a, b : Double) -> Type where
    MkBoundedDouble : (x : Double) 
                      -> {auto high : So (a <= x)}
                      -> {auto low : So (x <= b)}
                      -> BoundedDouble a b

Num (BoundedDouble a b) where
    (+) (MkBoundedDouble u) (MkBoundedDouble v) =
           let x = u + v
           in case (choose (a <= x), choose (x <= b)) of
             (Left _, Left _) => MkBoundedDouble x
             (Right _, _) => ?holeMin
             (_, Right _) => ?holeMax

Это уже проверки типов, но в нем есть дыры. Мы хотим установить ?holeMin на MkBoundedDouble a и ?holeMax на MkBoundedDouble b. Однако MkBoundedDouble сейчас нужны два доказательства: high и low. В случае ?holeMax это будут x = b So (a <= b) и So (b <= b). Опять же, Идрис не знает, что b <= b на каждые b : Double. Поэтому нам нужно будет снова выбрать, чтобы получить эти доказательства:

             (_, Right _) => case (choose (a <= b), choose (b <= b)) of
                  (Left _, Left _) => MkBoundedDouble b
                  _ => ?what

Поскольку Идрис не видит этого b <= b, функция будет частичной. Мы могли бы обмануть и использовать, например, MkBoundedDouble u в ?what, поэтому функция будет проверять тип и надеяться, что этого действительно никогда не произойдет.

Также есть возможность убедить контролера типов с силой, что b <= b всегда истинно:

data BoundedDouble : (a, b : Double) -> Type where
    MkBoundedDouble : (x : Double) 
                      -> {auto rightSize : So (a <= b)}
                      -> {auto high : So (a <= x)}
                      -> {auto low : So (x <= b)}
                      -> BoundedDouble a b

DoubleEqIsSym : (x : Double) -> So (x <= x) 
DoubleEqIsSym x = believe_me (Oh)

Num (BoundedDouble a b) where
    (+) (MkBoundedDouble u) (MkBoundedDouble v) =
           let x = u + v
           in case (choose (a <= x), choose (x <= b)) of
             (Left _, Left _) => MkBoundedDouble x
             (Right _, _) => MkBoundedDouble a {high=DoubleEqIsSym a}
             (_, Right _) => MkBoundedDouble b {low=DoubleEqIsSym b}

Или мы могли бы быть еще безопаснее и поместить доказательства для верхней и нижней границ в конструктор данных, чтобы мы могли использовать их в ?holeMin и ?holeMax. Это было бы:

import Data.So

data BoundedDouble : (a, b : Double) -> Type where
    MkBoundedDouble : (x : Double) 
                      -> {auto rightSize : So (a <= b)}
                      -> {auto leftId : So (a <= a)}
                      -> {auto rightId : So (b <= b)}
                      -> {auto high : So (a <= x)}
                      -> {auto low : So (x <= b)}
                      -> BoundedDouble a b

Num (BoundedDouble a b) where
    (+) (MkBoundedDouble u) (MkBoundedDouble v) =
           let x = u + v
           in case (choose (a <= x), choose (x <= b)) of
             (Left _, Left _) => MkBoundedDouble x
             (Right _, _) => MkBoundedDouble a
             (_, Right _) => MkBoundedDouble b

Вы видите, что даже то, что конструктор упакован доказательствами, они не усложняют реализацию. И они должны быть стерты в реальном коде времени выполнения.

Однако в качестве упражнения вы можете попробовать реализовать Num для

data BoundedDouble : (a, b : Double) -> Type where
    MkBoundedDouble : (x : Double)
                      -> {auto rightSize : So (a <= b)}
                      -> {auto high : So (a <= x)}
                      -> {auto low : So (x <= b)} 
                      -> BoundedDouble a b
    Min : {auto rightSize : So (a <= b)} -> BoundedDouble a b
    Max : {auto rightSize : So (a <= b)} -> BoundedDouble a b

К сожалению, ресурсов для Идриса пока не так много. Помимо учебника в разработке находится книга, которую я рекомендую. Это дает более доступные упражнения, чем работа с примитивными типами. :-)