## 我能向检验员提供关于ghc 7.6中归纳自然的证明吗？内容来源于 Stack Overflow，并遵循CC BY-SA 3.0许可协议进行翻译与使用

• 回答 (1)
• 关注 (0)
• 查看 (18)

GHC 7.6.1提供了用于类型级别编程的新特性，包括数据类型提升。以类型级自然和向量为例，我希望能够用依赖于算术基本定律的向量来编写函数。

```{-# 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 个回答

```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```

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

```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```

```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')```