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

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 arithmetic is defined with primitive functions. Идрис не может даже доказать, что 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 

Это уже typechecks, но в нем есть отверстия. Мы хотим установить ?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 

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