比较固定大小的矢量

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'看看例如附加类型级编号列表和TypeLits作为解释,以及可能的出路(即同时具有Peano风格的自然和仍然可以使用文字像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

10月'14 状态报告的ghc说:

Iavor Diatchki正致力于在GHC的约束求解器中使用现成的SMT求解器.目前,主要关注点是改进对类型级自然数的推理支持[...]

所以你的例子可能适用于ghc 7.10或7.12!