我可以在GHC 7.6中为类型检查器提供有关感应自然的证据吗？

Question

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

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