3

我一直在尝试一些 Haskell，因为我对强类型很感兴趣，但我对解决这个问题的最佳方法感到困惑：

Data.Vector 中定义的 Vector 数据类型允许通过嵌套数组的方式进行多维数组。但是，这些是由列表构成的，并且不同长度的列表被认为是相同的数据类型（与不同长度的元组不同）。

我如何扩展这种以相同方式起作用的数据类型（或编写类似的数据类型），除了不同长度的向量被认为是不同的数据类型，因此任何尝试创建具有不同长度行的多维数组/矩阵（对于例如）会导致编译时错误？

元组似乎通过写出 63 个不同的定义（每个有效长度一个）来管理这一点，但如果可能的话，我希望能够处理任意长度的向量。

4

2 回答 2

2

这种类型取决于值的类型通常称为依赖类型编程，幸运的是，Wolfgang Jeltsch使用 GADT 和 TypeFamilies 在 Haskell 中写了一篇关于依赖类型的博客文章。

这篇博文的要点是，如果我们有两种表示自然数的类型：

data Zero
data Succ nat

可以通过以下方式构建具有类型强制长度的列表：

data List el len where
   Empty :: List el Zero
   cons  :: el -> List el nat -> List el (Succ nat)
于 2012-05-14T07:48:34.833 回答
2

我看到了两种方法：

1）“类型化”方式：使用依赖类型。在某种程度上，这在 Haskell 中是可能的，最近 GHC 扩展为DataKinds*. 更好的是，使用具有真正高级类型系统的语言，例如 Agda。

2）另一种方式：编码你的向量，如

data Vec a = {values :: [a], len :: [Int]}

然后，只导出

buildVec :: [a] -> Vec a
buildVec as = Vec as (length as)

并检查使用相同长度向量的其他函数中的正确长度，例如确保矩阵函数或Vec加法中的相同长度向量。甚至更好：为矩阵提供另一个自定义构建器/ctor。

*我刚刚看到：您想要的正是DataKinds.

于 2012-05-14T05:57:22.463 回答