Доказательство коммутативности сложения на уровне типов натуральных чисел - PullRequest
Новая
       80

Доказательство коммутативности сложения на уровне типов натуральных чисел

0 голосов
/ 10 июня 2018

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

data Nat where
    Z :: Nat
    S :: Nat -> Nat

type family (a :: Nat) + (b :: Nat) :: Nat where
    Z + n = n
    S m + n = S (m + n)

data Vector (n :: Nat) a where
    Nil :: Vector Z a
    Cons :: a -> Vector n a -> Vector (S n) a

Кроме того, я создал функцию append, которая принимает m-вектор, n-вектор и возвращает (m + n) -вектор.Это работает так, как можно надеяться.Однако, просто ради этого, я попытался перевернуть его, чтобы он возвращал (n + m) -вектор.Это приводит к ошибке компилятора, потому что GHC не может доказать, что мое добавление коммутативно.Я все еще относительно новичок в семействах типов, поэтому я не уверен, как написать это доказательство самостоятельно, или, если это вообще можно сделать в haskell.

Сначала я думал как-то использовать равенство типовограничение, но я не уверен, как двигаться вперед.

Итак, чтобы быть ясным: я хочу написать эту функцию 

append :: Vector m a -> Vector n a -> Vector (n + m) a
append Nil xs         = xs
append (Cons x xs) ys = x `Cons` append xs ys

, но она не компилируется с 

    * Could not deduce: (n + 'Z) ~ n
      from the context: m ~ 'Z
        bound by a pattern with constructor: Nil :: forall a. Vector 'Z a,
                 in an equation for `append'

1 Ответ

0 голосов
/ 11 июня 2018

Вот полное решение.Предупреждение: включает в себя некоторые хасохизмы.

Мы начинаем как в исходном коде. 

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, GADTs, PolyKinds #-}
{-# OPTIONS -Wall -O2 #-}
module CommutativeSum where

data Nat where
    Z :: Nat
    S :: Nat -> Nat

type family (a :: Nat) + (b :: Nat) :: Nat where
    'Z + n = n
    'S m + n = 'S (m + n)

data Vector (n :: Nat) a where
    Nil :: Vector 'Z a
    Cons :: a -> Vector n a -> Vector ('S n) a

Старое добавление, тип которого проверяется немедленно. 

append :: Vector m a -> Vector n a -> Vector (m + n) a
append Nil xs         = xs
append (Cons x xs) ys = x `Cons` append xs ys

Для другого добавлениянам нужно доказать, что сложение коммутативно.Мы начнем с определения равенства на уровне типов, используя GADT. 

-- type equality, also works on Nat because of PolyKinds
data a :~: b where
   Refl :: a :~: a

Мы вводим одноэлементный тип, чтобы мы могли передавать Nat s и сопоставление с ними по шаблону. 

-- Nat singleton, to reify type level parameters
data NatI (n :: Nat) where
  ZI :: NatI 'Z
  SI :: NatI n -> NatI ('S n)

Мы можем связать с каждым вектором его длину как синглтон NatI. 

-- length of a vector as a NatI
vecLengthI :: Vector n a -> NatI n
vecLengthI Nil = ZI
vecLengthI (Cons _ xs) = SI (vecLengthI xs)

Теперь основная часть.Нам нужно доказать n + m = m + n по индукции.Это требует нескольких лемм для некоторых арифметических законов. 

-- inductive proof of: n + Z = n  
sumZeroRight :: NatI n -> (n + 'Z) :~: n
sumZeroRight ZI = Refl
sumZeroRight (SI n') = case sumZeroRight n' of
   Refl -> Refl

-- inductive proof of: n + S m = S (n + m)
sumSuccRight :: NatI n -> NatI m -> (n + 'S m) :~: 'S (n + m)
sumSuccRight ZI _m = Refl
sumSuccRight (SI n') m  = case sumSuccRight n' m of
   Refl -> Refl

-- inductive proof of commutativity: n + m = m + n
sumComm :: NatI n -> NatI m -> (n + m) :~: (m + n)
sumComm ZI m = case sumZeroRight m of Refl -> Refl
sumComm (SI n') m = case (sumComm n' m, sumSuccRight m n') of
   (Refl, Refl) -> Refl

Наконец, мы можем использовать приведенное выше доказательство, чтобы убедить GHC набрать append, как мы и хотели.Обратите внимание, что мы можем повторно использовать реализацию со старым типом, а затем убедить GHC, что он также может использовать новый. 

-- append, with the wanted type
append2 :: Vector m a -> Vector n a -> Vector (n + m) a
append2 xs ys = case sumComm (vecLengthI xs) (vecLengthI ys) of
   Refl -> append xs ys

Заключительные замечания.По сравнению с полностью зависимым типом языка (скажем, типа Coq) нам пришлось вводить синглтоны и тратить больше усилий, чтобы заставить их работать («болезненная» часть хасохизма).В свою очередь, мы можем просто сопоставить шаблон с Refl и позволить GHC выяснить, как использовать выведенные уравнения, не вмешиваясь в зависимое сопоставление (часть «удовольствия»).

В целом, я думаю, что все еще немного легче работать с полностью зависимыми типами.Если / когда GHC получит не стертые квантификаторы типов (pi n. ... за пределами forall n. ...), возможно, Haskell станет более удобным.

...