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

【问题标题】：Converting a list to a type-safe vector将列表转换为类型安全的向量
【发布时间】：2014-05-30 19:10:13
【问题描述】：

我正在尝试编写函数

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.

我相信由于(:|) 的类型签名而引发了错误。

有没有办法绕过这个错误？

【问题讨论】：

标签： haskell

【解决方案1】：

错误是您的类型签名在n 中普遍量化，即它说“对于任何n，我们可以从列表中构建一个长度为n 的向量”。不兼容的是，函数定义声明向量始终具有给定列表的长度。

基本上，您需要存在量化 来定义这个函数（“根据列表长度，会有一个n 使得n 是结果向量的长度”）。昨天才讨论过，you can't have existentially-quantified type variables in a signature。你可以拥有的是存在类型——最好还是写成 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

【讨论】：

感谢您的回答 - 不幸的是，我相信我以这种方式失去了对向量大小的所有概念，所以它并没有比没有实现 fromList 好多少...
嗯，是的，有点。但这是不可避免的，在您从一个没有任何类型保证长度保证的类型 start 之后。
这是有道理的。有没有办法将另一个参数作为列表的长度传递？
您已经使用原始签名做到了这一点：n 本质上是传递到函数的编译时参数。实际上，您可以通过这种方式实现该函数（您需要一个类型类来确保只传入自然数，而不是其他垃圾），但这也不安全：实际上无法确保给定列表有合适的长度。（你可以做的是，循环和切断 - 实际上使用non-empty list 是安全的。）