我可以向类型检查器提供GHC 7.6中归纳自然数的证明吗？
GHC7.6.1为类型级别的编程带来了新特性，包括datatype promotion。以类型级自然变量和向量为例，我希望能够在依赖于基本算术法则的向量上编写函数。
不幸的是，尽管我想要的规则通常很容易通过案例分析和归纳在归纳自然语言上得到证明，但我怀疑我能否说服类型检查员相信这一点。作为一个简单的例子，下面的反向函数的类型检查需要一个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
Stack Overflow用户
发布于 2012-09-16 09:33:05
(注意:我只对这些代码进行了类型检查(而不是实际运行)。)
方法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，这是我们需要知道的，以便在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')方法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 xs@(Cons {}) = case initLast xs of
(x, xs') -> Cons x (rev xs')https://stackoverflow.com/questions/12442858
复制相似问题