比较固定大小的向量

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+1) ~ (n'+1) 推导出类型相等 n ~ n' 虽然从 S n ~ S n' 中推导出它没有问题，请参见例如Append for type-level numbered lists with TypeLits 的解释和可能的出路（即既有 Peano 风格的自然字，又能使用像 5 这样的文字）

但是，如果您将 Nvector 的定义更改为

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

它必须从n ~ n'推导n-1 ~ n'-1，推导容易多了！这会编译，并且仍然会产生正确的类型，例如Cons () Nil:

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

请注意，这没什么用，因为我们仍然无法定义

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

14 年 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！

比较固定大小的向量

Compare fixed sized vectors

haskell