Доказательство m + (1 + n) == 1+ (m + n) в зависимом хаскеле - PullRequest
Новая
       29

Доказательство m + (1 + n) == 1+ (m + n) в зависимом хаскеле

0 голосов
/ 17 января 2019

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

{-# language TypeFamilies, KindSignatures, DataKinds, PolyKinds, UndecidableInstances, GADTs #-}

data Nat = Zero | Succ Nat deriving Show
type family Add (m :: Nat) (n :: Nat) :: Nat where
  Add Zero n = n
  Add (Succ m) n = Add m (Succ n)

data SNat :: Nat -> * where
  Zy :: SNat Zero
  Suc :: SNat m -> SNat (Succ m)

data Bounded' m = B m

sum' :: Bounded' (SNat m) -> Bounded' (SNat n) -> Bounded' (SNat (Add m n))
sum' (B m) (B n) = B $ case (m, n) of
                    (Zy,x) -> x
                    (Suc x, y) -> let B z = sum' (B x) (B y) in Suc z

Вот ошибка: 

    • Could not deduce: Add m1 ('Succ n) ~ 'Succ (Add m1 n)
      from the context: m ~ 'Succ m1
      bound by a pattern with constructor:
               Suc :: forall (m :: Nat). SNat m -> SNat ('Succ m),
               in a case alternative
      at main.hs:17:22-26
      Expected type: SNat (Add m n)
      Actual type:   SNat ('Succ (Add m1 n))
    • In the expression: Suc z
      In the expression: let B z = sum' (B x) (B y) in Suc z
      In a case alternative:
        (Suc x, y) -> let B z = sum' (B x) (B y) in Suc z

Я понимаю сообщение об ошибке. Как я могу предоставить GHC необходимое доказательство того, что Add m n = Succ (Add k n) в выражении Suc z, когда он узнает, что m ~ Succ k (во втором случае соответствует), и существуют ли альтернативные подходы к этому. Спасибо.

1 Ответ

0 голосов
/ 17 января 2019

Ваше определение сложения не является общепринятым. 

type family Add (m :: Nat) (n :: Nat) :: Nat where
  Add Zero n = n
  Add (Succ m) n = Add m (Succ n)

Это "хвостовое рекурсивное" добавление.Кажется, кажется, что должен быть способ доказать свои свойства, используя эту форму добавления, но я не могу понять это.До тех пор с хвостовой рекурсией на уровне типа / свойства обычно работать гораздо сложнее, чем со стандартным: 

type family Add (m :: Nat) (n :: Nat) :: Nat where
  Add Zero n = n
  Add (Succ m) n = Succ (Add m n)

Последнее определение сложения делает ваш sum' проход без каких-либо убедительныхвсе.

РЕДАКТИРОВАТЬ на самом деле это было легко, как только я увидел это правильно.Вот что я получил (импортировал Data.Type.Equality и включил LANGUAGE TypeOperators): 

propSucc2 :: SNat m -> SNat n -> Add m (Succ n) :~: Succ (Add m n)
propSucc2 Zy _ = Refl
propSucc2 (Suc m) n = propSucc2 m (Suc n)

Хвосто-рекурсивное определение, хвост-рекурсивное доказательство.Затем, чтобы использовать его, вы используете gcastWith: 

sum' (B m) (B n) = ...
        (Suc x, y) -> gcastWith (propSucc2 x y) 
                                (let B z = sum' (B x) (B y) in Suc z)

gcastWith просто берет равенство :~: и делает его доступным для средства проверки типов в рамках его второго аргумента.

Кстати, если вы определите sum' в параллельной структуре для вашего семейства типов Add, тогда вам не нужны никакие леммы.Заставить вещи следовать параллельным структурам - хорошая техника, чтобы упростить задачу (это часть искусства зависимого программирования, поскольку не всегда очевидно, как): 

sum' :: Bounded' (SNat m) -> Bounded' (SNat n) -> Bounded' (SNat (Add m n))
sum' (B Zy) (B n) = B n
sum' (B (Suc m)) (B n) = sum' (B m) (B (Suc n))
...