相关疑难解决方法(0)

我正在尝试为Haskell中的固定长度列表定义一个类型.当我使用标准方式将自然数编码为一元中的类型时,一切正常.但是,当我尝试在GHC的类型文字上构建所有内容时,我遇到了大量问题.

我对所需列表类型的第一次拍摄是

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

遗憾的是,它不允许使用类型编写zip函数

zip :: List n a -> List n b -> List n (a,b)

我可以通过从类型变量n中的类型变量中减去1来解决这个问题(:>):

data List (n :: Nat) a where
  Nil :: List 0 a
  (:>) :: a -> List (n-1) a -> List n a -- subtracted 1 from both n's

接下来,我尝试定义一个追加函数:

append :: List n1 a -> …

我正在尝试写一个固定大小的矢量,如下所示:

{-# 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 …