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

Question

Я новичок в Идрисе. Мне нужно создать данные, описывающие ограниченное число. Итак, я сделал такие данные с помощью такого конструктора:

data BoundedDouble : (a, b : Double) -> Type where
  MkBoundedDouble : (x : Double) -> 
                    {auto p : a <= x && x <= b = True} -> 
                    BoundedDouble a b

Кажется, чтобы создать Double между a а также b, А вот простой пример использования:

test : BoundedDouble 0.0 1.0
test = MkBoundedDouble 0.0 

Оно работает. Но сейчас я хочу реализовать Num интерфейс для BoundedDouble, Я попробовал это:

Num (BoundedDouble a b) where
  (MkBoundedDouble x) + (MkBoundedDouble y) = 
    MkBoundedDouble (ifThenElse (x + y > b) 
                      (x + y - (b - a))
                      (ifThenElse (x + y < a)
                        (x + y + (b - a))
                        (x + y)))

Но это не работает, я думаю, почему, но я не могу это объяснить. Как я должен реализовать дополнение?

Я не знаю точно, что я должен делать или читать, чтобы понять это.

Answer 1

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

При работе с такими слепыми доказательствами времени выполнения (так просто … = True), Data.So довольно полезно. 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 = bSo (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

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