为了避免参差不齐的矩阵，我想为包含类型长度的列表设计一个类型包装器。 （如果我不称之为“长度索引向量”，请纠正我。）我想将它作为一个带有智能构造函数的抽象类型提供，其中包括IsList实例或类似的精神。
这就是我所在的地方：
data Nat = Z | S Nat
data Vector (n :: Nat) a = Vector [a] deriving Show
v0 :: Vector Z a
v0 = Vector [ ]
put :: a -> Vector n a -> Vector (S n) a
put x (Vector xs) = Vector (x:xs)
class Fold a where
type Elem a
fold :: [Elem a] -> a
instance Fold (Vector Z a) where
type Elem (Vector Z a) = a
fold [ ] = v0
instance Fold (Vector (S n) a) where
type Elem (Vector (S n) a) = a
fold (x:xs) = put x (fold xs)
Fold类型类应该逐个从列表中获取元素，并将put它们添加到向量中。我打算用Naturals代表基础案例和结构归纳的归纳案例。
但是，我发布的代码不起作用，我无法排除错误。本质上，它讨论了不同长度的向量的元素类型不相等：
...
Expected type: [Elem (Vector n a)]
Actual type: [Elem (Vector ('S n) a)]
...
fold (x:xs) = put x (fold xs)
^^
如果我假设神奇的强制功能：
fold (x:xs) = put x (fold $ undefined xs)
- 然后我会遇到另一个错误：
• No instance for (Fold (Vector n a)) arising from a use of ‘fold’
...
fold (x:xs) = put x (fold $ undefined xs)
^^^^^^^^^^^^^^^^^^^
这让我很难过，因为它必然意味着我的归纳实例不会迭代。
我需要帮助。
IsList实例吗？编译器通知您两个不同的问题。
本质上，它讨论了不同长度的向量的元素类型不相等：
发现！你有两种方法。如果你想让Elem家族成为类型类的一部分，你必须在归纳案例中添加一个额外的约束，基本上告诉GHC“我的元素类型相等”：
instance (Elem (Vector n a) ~ a) => Fold (Vector (S n) a) where
type Elem (Vector (S n) a) = a
fold (x:xs) = put x (fold xs)
或者，您可以使该类型族完全分离，并且只有一个（更明智的）实例：
type family Elem xs :: *
type instance Elem (Vector n x) = x
class Fold a where
fold :: [Elem a] -> a
由你决定！
这让我很难过，因为它必然意味着我的归纳实例不会迭代。
当然它没有“迭代”，因为你没有告诉GHC去找一个递归的子问题！只需将该子问题添加到您对感应案例的约束中。
-- If you decided to keep the type family associated
instance (Elem (Vector n a) ~ a, Fold (Vector n a)) => Fold (Vector (S n) a) where
type Elem (Vector (S n) a) = a
fold (x:xs) = put x (fold xs)
要么
-- If you decided not to keep the type family associated
instance Fold (Vector n a) => Fold (Vector (S n) a) where
fold (x:xs) = put x (fold xs)
我可以获得[
IsList实例]吗？
没有.IsList a暗示功能[Elem a] -> a。对于长度索引向量，这是不可能的，因为签名要求输出类型不依赖于输入长度。你可以得到的最接近的是：
data VecSomeLen a = forall (n :: Nat). VecSomeLen (Vector n a)
instance IsList (VecSomeLen a) where ...
-- and also
instance IsList (Maybe (Vector n a)) where ...
它并非完全无用，因为它将没有大小的列表提升到一个具有未知但可操作大小的列表/检查列表是否具有给定长度，但是当您认为通常在大小已知时使用它时它是无用的。
我只是使用varargs。
-- untested but *should* compile
class MkVector n a n' r | r -> n a n' where
mkVector :: (Vector n a -> Vector n' a) -> r
instance MkVector Z a n (Vector n a) where
mkVector f = f $ Vector []
instance (MkVector n a n' r) => MkVector (S n) a n' (a -> r) where
mkVector f x = mkVector $ \(Vector xs) -> f $ Vector $ x:xs
vector :: MkVector n a n r => r
vector = mkVector id
-- vector 1 5 3 :: Vector (S(S(S(Z)))) Int
现在，问题是你的Fold类虽然可以用@Alec的变化编译，但完全是错的。查看您要创建的函数的类型：
fold :: forall n. [a] -> Vector n a
那不好！给定一个元素列表，您可以创建一个大小的列表，除了新大小与输入列表无关。你好像用非整体来解决这个问题，这只是一个可怕的想法。此外，如果任何人过来并试图使fold总计，很容易打破Vector不变量的意外。老实说，你对Vector的定义有点奇怪。打破其不变量很容易，因为支持数据的界面类型不像其界面那样强。我重新定义它：
data Vector (n :: Nat) a where
(:%:) :: a -> Vector n a -> Vector (S n) a
VNil :: Vector Z a
infixr 5 :%:
-- infixr 5 :
这使得无法编写总fold（这很好，因为它的存在是一个错误）。但是，您不能（安全地）强制执行正常列表，因为这不再是新类型（但我相信他们仍然具有相同的表示，并且仍然可以是unsafeCoerce）。
更好的想法是用Maybe编码偏好。此外，您可以从Fold类中抽象出某个模式，以便更轻松地编写类似的函数。
-- can’t match on types so match on SNat representatives
data SNat (n :: Nat) where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
-- pass SNats around implicitly
class KNat (n :: Nat) where kNat :: SNat n
instance KNat Z where kNat = SZ
instance KNat n => KNat (S n) = SS kNat
fromList' :: SNat n -> [a] -> Maybe (Vector n a)
fromList' (SS n) (x:xs) = (x :%:) <$> fromList' n xs
fromList' SZ [] = return VNil
fromList' _ _ = Nothing
fromList :: KNat n => [a] -> Maybe (Vector n a)
fromList = fromList' kNat