将列表转换为类型安全的向量

Question

我正在尝试编写该函数

fromList :: [e] -> Vector n e
fromList [] = Nil
fromList (x:xs) = x :| fromList xs

使用这个向量的定义

data Natural where
    Zero :: Natural
    Succ :: Natural -> Natural

data Vector n e where
  Nil  :: Vector Zero e
  (:|) :: e -> Vector n e -> Vector (Succ n) e

infixr :|

但是,Haskell给出了错误

    Couldn't match type 'Zero with 'Succ n0
    Expected type: Vector n e
      Actual type: Vector ('Succ n0) e
    In the expression: x :| fromList xs
    In an equation for `fromList': fromList (x : xs) = x :| fromList xs
Failed, modules loaded: none.

我相信错误是因为类型签名而引发的(:|).

有没有办法解决这个错误？

Answer 1

错误是您的类型签名是普遍量化的n,即它表示"对于任何n,我们可以n从列表中构建长度向量".与此不同,函数定义表明向量始终具有给定列表的长度.

基本上,您需要存在量化来定义此函数("取决于列表长度,将有一个n这样n的结果向量的长度").仅在昨天讨论过,您不能在签名中使用存在量化的类型变量.你可以拥有的是存在主义类型 - 最好再写为GADT,

data DynVector e where
  DynVector :: Vector n e -> DynVector e

然后你可以定义

fromList' :: [e] -> DynVector e
fromList' [] = DynVector Nil
fromList' (x:xs) = case fromList xs of
   DynVector vs -> DynVector $ x :| vs