haskell - 好的类型系统可以区分不同基数的矩阵吗？

Question

我的程序(Hartree-Fock/iterative SCF)有两个矩阵 F 和 F'，它们实际上是用两种不同基数表示的相同矩阵。我刚刚损失了三个小时的调试时间，因为我不小心使用了 F' 而不是 F。在 C++ 中，类型检查器不会捕获此类错误，因为两个变量都是 Eigen::Matrix<double, 2, 2>对象。

我想知道，对于 Haskell/ML/等等。大家，如果您正在编写这个程序，您是否会构建一个类型系统，其中 F 和 F' 具有不同的类型？那会是什么样子？我基本上是想了解如何将一些逻辑错误外包给类型检查器。

编辑:矩阵的基础就像单位。你可以说 1L，也可以说多少加仑，它们的意思是一样的。或者，举一个向量示例，您可以在笛卡尔坐标中说 (0,1) 或在极坐标中说 (1,pi/2)。但即使含义相同，数值却不同。

编辑:也许单位是错误的类比。我不是在寻找某种记录类型，我可以在其中指定第一个字段为升，第二个字段为加仑，而是寻找一种方式来表示这个矩阵作为一个整体，是根据其他一些矩阵定义的(基)，其中基可以是任何相同维度的矩阵。例如，构造函数看起来像 mkMatrix [[1, 2], [3, 4]] [[5, 6], [7, 8]]然后将该对象添加到另一个矩阵中，仅当两个对象的第二个参数具有相同的矩阵时才会进行类型检查。这有道理吗？

编辑:Wikipedia 上的定义, worked examples

Answer 1

这在 Haskell 中是完全可能的。

静态检查尺寸

Haskell 的数组带有 statically checked dimensions ，可以静态地操作和检查维度，防止索引到错误的维度。一些例子:

这只有效on 2-D arrays :

multiplyMM :: Array DIM2 Double -> Array DIM2 Double -> Array DIM2 Double

来自 repa 的示例应该能让您有所了解。这里，取对角线需要一个二维数组，返回一个相同类型的一维数组。

diagonal :: Array DIM2 e -> Array DIM1 e

或者，来自Matt sottile's repa tutorial ，3D 矩阵变换上的静态检查尺寸:

f :: Array DIM3 Double -> Array DIM2 Double
f u =
  let slabX = (Z:.All:.All:.(0::Int))
      slabY = (Z:.All:.All:.(1::Int))
      u' = (slice u slabX) * (slice u slabX) +
           (slice u slabY) * (slice u slabY)
  in
    R.map sqrt u'

静态检查单位

矩阵编程之外的另一个示例:静态检查 units of dimension ，使其成为令人困惑的类型错误，例如英尺和米，无需进行转换。

 Prelude> 3 *~ foot + 1 *~ metre
 1.9144 m

或整套SI units and quanities 。

例如无法添加不同尺寸的东西，例如体积和长度:

> 1 *~ centi litre + 2 *~ inch 
Error:
Expected type: Unit DVolume a1
  Actual type: Unit DLength a0

所以，关注the repa-style array dimension types ，我建议向您的数组类型添加一个 Base 幻像类型参数，并使用它来区分基数。在 Haskell 中，索引 Dim类型参数给出了数组的等级(即它的形状)，你也可以做类似的事情。

或者，如果基数是指单位上的某个维度，则使用维度类型。

所以，是的，这现在几乎是 Haskell 中的一种商品技术，并且有一些使用此类类型进行设计的示例来帮助您入门。