haskell - 将列表转换为具有类型约束的固定长度的列表

Question

让我定义一个长度受限的列表。IE

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

然后我想从普通列表中初始化这个列表（例如任意长度的输入字符串）。我可以这样做吗？是否可以像这样编写函数（或类）？

toConsList :: [a] -> List n a

或者这是否仅适用于编译时已知长度的结构？

score 2 · Accepted Answer

你不能，因为那需要依赖类型。结果的类型List 取决于value。_ 正如您的类型错误所示，您不能使用foldr Cons Nil（这将是显而易见的实现）来创建列表，因为累加器必须在整个折叠中保持相同的类型。

正如@chi 在评论中指出的那样，您可以使用存在包装器来忽略类型参数以使其工作。你最终会得到一个未知List n a的值，这对你来说没有任何好处。 n[a]

有Data.Vector.Fixed.fromList，但那里的文档告诉我们它“如果列表比结果向量短，将抛出错误”。这意味着它实际上只是要求您在编译时指定向量（列表）的类型（长度），如果不满足该期望，则在运行时截断或抛出错误。

您可能对 Idris 感兴趣Data.Vect.Vect。

1 回答 1