具有编译器强制长度的 Haskell 多维数组

Question

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

Data.Vector 中定义的 Vector 数据类型允许通过嵌套数组的方式创建多维数组。但是，它们是从列表构造的，并且不同长度的列表被视为相同的数据类型(与不同长度的元组不同)。

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

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

Answer 1

我看到有两种方法可以做到这一点:

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 的标准示例。