Могу ли я предоставить средство проверки типов с доказательствами об индуктивных натуралах в GHC 7.6?

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

К сожалению, несмотря на то, что законы, которые я хочу, обычно легко доказывать на индуктивных naturals анализом случая и индукцией, я сомневаюсь, что я могу убедить в этом. В качестве простого примера для проверки наивной обратной функции ниже требуется подтверждение того, что n + Su Ze ~ Su n.

Есть ли способ предоставить это доказательство, или я действительно сейчас в области полномасштабных зависимых типов?

{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeFamilies, TypeOperators #-}

data Nat = Ze | Su Nat

data Vec :: * -> Nat -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

type family (m :: Nat) + (n :: Nat) :: Nat

type instance Ze + n = n
type instance (Su m + n) = Su (m + n)

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

rev :: Vec a n -> Vec a n
rev Nil = Nil
rev (Cons x xs) = rev xs `append` Cons x Nil

Ответы

Ответ 1

(Примечание. У меня есть только проверенный тип (и фактически не выполняемый) любого из этого кода.)

Подход 1

Собственно, вы можете манипулировать доказательствами, сохраняя их в GADT. Чтобы этот подход работал, вам нужно включить ScopedTypeVariables.

data Proof n where
    NilProof  :: Proof Ze
    ConsProof :: (n + Su Ze) ~ Su n => Proof n -> Proof (Su n)

class PlusOneIsSucc n where proof :: Proof n
instance PlusOneIsSucc Ze where proof = NilProof
instance PlusOneIsSucc n => PlusOneIsSucc (Su n) where
    proof = case proof :: Proof n of
        NilProof    -> ConsProof proof
        ConsProof _ -> ConsProof proof

rev :: PlusOneIsSucc n => Vec a n -> Vec a n
rev = go proof where
    go :: Proof n -> Vec a n -> Vec a n
    go NilProof Nil = Nil
    go (ConsProof p) (Cons x xs) = go p xs `append` Cons x Nil

На самом деле, возможно, интересная мотивация для типа Proof выше, я изначально имел только

data Proof n where Proof :: (n + Su Ze) ~ Su n => Proof n

Но это не сработало: GHC справедливо жаловался, что только потому, что мы знаем, что (Su n)+1 = Su (Su n) не означает, что мы знаем n+1 = Su n, что нам нужно знать, чтобы сделать рекурсивный вызов rev в случай Cons. Поэтому мне пришлось расширить значение a Proof, чтобы включить доказательство всех равенств для естественных чисел до и включив n - по существу аналогичную вещь для процесса упрощения при переходе от индукции к сильной индукции.

Подход 2

После небольшого раздумья я понял, что класс оказывается немного лишним; что делает этот подход особенно приятным, поскольку он не требует каких-либо дополнительных расширений (даже ScopedTypeVariables) и не вводит никаких дополнительных ограничений для типа Vec.

data Proof n where
    NilProof  :: Proof Ze
    ConsProof :: (n + Su Ze) ~ Su n => Proof n -> Proof (Su n)

proofFor :: Vec a n -> Proof n
proofFor Nil = NilProof
proofFor (Cons x xs) = let rec = proofFor xs in case rec of
    NilProof    -> ConsProof rec
    ConsProof _ -> ConsProof rec

rev :: Vec a n -> Vec a n
rev xs = go (proofFor xs) xs where
    go :: Proof n -> Vec a n -> Vec a n
    go NilProof Nil = Nil
    go (ConsProof p) (Cons x xs) = go p xs `append` Cons x Nil

Подход 3

В качестве альтернативы, если вы переключите реализацию rev немного на минус последний элемент на обратном начальном сегменте списка, тогда код может выглядеть немного более простым. (Этот подход также не требует дополнительных расширений.)

class Rev n where
    initLast :: Vec a (Su n) -> (a, Vec a n)
    rev :: Vec a n -> Vec a n

instance Rev Ze where
    initLast (Cons x xs) = (x, xs)
    rev x = x

instance Rev n => Rev (Su n) where
    initLast (Cons x xs) = case initLast xs of
        (x', xs') -> (x', Cons x xs')
    rev as = case initLast as of
        (a, as') -> Cons a (rev as')

Подход 4

Подобно подходу 3, но опять же, заметив, что классы типов не нужны.

initLast :: Vec a (Su n) -> (a, Vec a n)
initLast (Cons x xs) = case xs of
    Nil     -> (x, Nil)
    Cons {} -> case initLast xs of
        (x', xs') -> (x', Cons x xs')

rev :: Vec a n -> Vec a n
rev Nil = Nil
rev [email protected](Cons {}) = case initLast xs of
    (x, xs') -> Cons x (rev xs')