haskell - 比较固定大小的向量

Question

我正在尝试编写一个固定大小的向量，如下所示:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators #-}
import GHC.TypeLits

data NVector (n :: Nat) a where
    Nil :: NVector 0 a
    Cons :: a -> NVector n a -> NVector (n + 1) a

instance Eq a => Eq (NVector n a) where
    Nil == Nil = True
    (Cons x xs) == (Cons y ys) = x == y && xs == ys

但编译失败并显示以下消息:

 Could not deduce (n2 ~ n1)
from the context (Eq a)
  bound by the instance declaration at prog.hs:8:10-33
or from (n ~ (n1 + 1))
  bound by a pattern with constructor
             Cons :: forall a (n :: Nat). a -> NVector n a -> NVector (n + 1) a,
           in an equation for `=='
  at prog.hs:10:6-14
or from (n ~ (n2 + 1))
  bound by a pattern with constructor
             Cons :: forall a (n :: Nat). a -> NVector n a -> NVector (n + 1) a,
           in an equation for `=='
  at prog.hs:10:21-29

但是如果我手动引入类型级自然数，它会成功编译

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies #-}
data Nat = Z | S Nat

infixl 6 :+

type family   (n :: Nat) :+ (m :: Nat) :: Nat
type instance Z     :+ m = m
type instance (S n) :+ m = S (n :+ m) 

data NVector (n :: Nat) a where
    Nil :: NVector Z a
    Cons :: a -> NVector n a -> NVector (S n) a

instance (Eq a) => Eq (NVector n a) where
    Nil == Nil = True
    (Cons x xs) == (Cons y ys) = x == y && xs == ys

ghc版本7.8.3

Answer 1

ghc无法(还没有？)推断出类型相等 n ~ n'来自(n+1) ~ (n'+1)虽然从 S n ~ S n' 中推导出它没有任何问题。参见例如Append for type-level numbered lists with TypeLits寻求解释和可能的出路(即拥有皮亚诺风格的自然数，并且仍然能够使用像 5 这样的文字)

但是，如果您更改 Nvector 的定义进入

data NVector (n :: Nat) a where
    Nil :: NVector 0 a
    Cons :: a -> NVector (n -1) a -> NVector n a

它必须推断出n-1 ~ n'-1来自n ~ n' ，更容易推演!编译后，仍然会产生正确的类型，例如Cons () Nil :

*Main> :t Cons () Nil
Cons () Nil :: NVector 1 ()

请注意，这几乎没有用，因为我们仍然无法定义

append :: NVector n a -> NVector m a -> NVector (n + m) a -- won't work

2014 年 10 月 status report对于 ghc说:

Iavor Diatchki is working on utilizing an off-the-shelf SMT solver in GHC's constraint solver. Currently, the main focus for this is improved support for reasoning with type-level natural numbers [...]

所以您的示例可能可以在 ghc 7.10 或 7.12 上正常运行!