我能否在GHC 7.6中为类型检查器提供关于归纳自然数的证明？

Question

我能否在GHC 7.6中为类型检查器提供关于归纳自然数的证明？

19

GHC 7.6.1 带来了一些新的类型级编程特性，包括数据类型提升。从那里的关于类型级自然数和向量的例子中，我希望能够编写依赖于算术基本原理的向量函数。

不幸的是，即使我想要的定律通常可以通过对归纳自然数进行案例分析和归纳来轻松证明，但我怀疑我无法说服类型检查器做到这一点。作为一个简单的例子，检查下面的天真反转函数需要证明 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

- GS - Apologise to Monica

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Daniel Wagner · Accepted Answer

（注意：我只对这段代码进行了类型检查，而没有真正运行它。）

方法1

实际上，您可以通过将证明存储在GADTs中来操纵证明。为使此方法有效，您需要打开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，这正是我们需要知道的，以便在 Cons 情况下进行递归调用rev。因此，我不得不扩展 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')

方法四

与方法三类似，但再次注意到类型类是不必要的。

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 xs@(Cons {}) = case initLast xs of
    (x, xs') -> Cons x (rev xs')