Wan*_*ang 29 ocaml haskell types type-systems sml
我的程序(Hartree-Fock /迭代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]],然后将该对象添加到另一个矩阵只有当两个对象具有与其第二个参数相同的矩阵时才进行类型检查.那有意义吗？
Don*_*art 19
这在Haskell中是完全可能的.
静态检查尺寸
Haskell具有静态检查维度的数组,其中维度可以被静态操作和检查,从而防止索引到错误的维度.一些例子:
这只适用于二维数组:
multiplyMM :: Array DIM2 Double -> Array DIM2 Double -> Array DIM2 Double
一个例子repa应该给你一个感觉.这里,采用对角线需要2D数组,返回相同类型的1D数组.
diagonal :: Array DIM2 e -> Array DIM1 e
或者,从Matt sottile的修复教程中,在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'
静态检查单位
矩阵编程之外的另一个例子:静态检查维度单位,使其成为混淆例如英尺和米的类型错误,而不进行转换.
Prelude> 3 *~ foot + 1 *~ metre
1.9144 m
或者用于整套SI单位和数量.
例如,无法添加不同维度的内容,例如卷和长度:
> 1 *~ centi litre + 2 *~ inch
Error:
Expected type: Unit DVolume a1
Actual type: Unit DLength a0
所以,下面的repa风格阵列尺寸类型,我建议增加一个Base幻象类型参数的数组类型,并使用该基地进行区分.在Haskell中,索引Dim
类型参数给出了数组的等级(即它的形状),你也可以这样做.
或者,如果基数是指单位上的某个维度,则使用维度类型.
所以,是的,现在这几乎是Haskell中的一种商品技术,并且有一些使用这样的类型进行设计的例子可以帮助您入门.
gat*_*ado 16
这个问题问得好.我不认为你可以在大多数类型系统中编码基础的概念,因为类型检查器所做的任何事情都需要能够终止,并且判断两个实值向量是否相等是非常困难的.例如,您可以拥有(2 v_1)+(2 v_2)或2(v_1 + v_2).有些语言使用依赖类型 [ 维基百科 ],但这些是相对学术性的.
我认为,如果您只是编码矩阵与矩阵一起工作的基础,那么大多数调试工作都会得到缓解.例如,
newtype Matrix = Matrix { transform :: [[Double]],
srcbasis :: [Double], dstbasis :: [Double] }
然后,当你中号从基础一至b 与Ñ,检查Ñ是从b到c ^,并与基础返回一个矩阵一个到Ç.
注意 - 似乎这里的大多数人都有编程而不是数学背景,所以我在这里提供简短的解释.矩阵是向量空间之间的线性变换的编码.例如,如果你在R ^ 2(二维实数)中将旋转编码45度,那么在矩阵中对此进行编码的标准方法是说标准基矢量e_1,写为"[1,0] ",被发送到e_1和e_2的组合,即[1/sqrt(2),1/sqrt(2)].关键是你可以通过说出不同向量的位置来编码相同的旋转,例如,你可以说你发送[1,1]和[1,-1]的位置而不是e_1 = [1,0]和e_2 = [0,1],这将具有不同的矩阵表示.
如果你有一组有限的基础,你可以做到......
{-# LANGUAGE EmptyDataDecls #-}
data BasisA
data BasisB
data BasisC
newtype Matrix a b = Matrix { coefficients :: [[Double]] }
multiply :: Matrix a b -> Matrix b c -> Matrix a c
multiply (Matrix a_coeff) (Matrix b_coeff) = (Matrix multiplied) :: Matrix a c
where multiplied = undefined -- your algorithm here
然后,在ghci(交互式Haskell解释器)中,
*Matrix> let m = Matrix [[1, 2], [3, 4]] :: Matrix BasisA BasisB
*Matrix> m `multiply` m
<interactive>:1:13:
Couldn't match expected type `BasisB'
against inferred type `BasisA'
*Matrix> let m2 = Matrix [[1, 2], [3, 4]] :: Matrix BasisB BasisC
*Matrix> m `multiply` m2
-- works after you finish defining show and the multiplication algorithm
Bjö*_*ter 11
虽然我意识到这并没有严格解决(澄清的)问题 - 我的道歉 - 这似乎至少与Don Stewart的流行答案有关......
我是Don引用并提供示例的Haskell 维度库的作者.我也一直在写一些基于维度的实验性基本线性代数库.该线性代数库静态地跟踪矢量和矩阵的大小以及每个元素的元素的物理尺寸("单位").
最后一点 - 基于每个元素跟踪物理尺寸 - 相当具有挑战性,并且对于大多数用途而言可能是过度杀伤,甚至可以认为在任何给定的矢量/矩阵中将大量不同的物理尺寸作为元素几乎没有数学意义.然而,我感兴趣的一些线性代数应用,例如卡尔曼滤波和加权最小二乘估计,通常使用异构状态向量和协方差矩阵.
使用卡尔曼滤波器作为示例,考虑具有物理尺寸[L,LT ^ -1]的状态向量x = [d,v ].通过乘以状态转移矩阵F来预测下一个(未来)状态向量,即:x'= F x_.很明显,这个等式有意义F不能是任意的,但必须有尺寸和物理尺寸[[1,T],[T ^ -1,1]].以下predict_x'函数静态地确保此关系成立:
predict_x' :: (Num a, MatrixVector f x x) => Mat f a -> Vec x a -> Vec x a
predict_x' f x_ = f |*< x_
(难看的运算符|*<表示左边的矩阵乘以右边的向量.)
更一般地,对于x_任意大小的先验状态向量并且具有任意物理维度的元素,传递f具有"不兼容"大小和/或物理维度的状态转移矩阵predict_x'将导致编译时间错误.
在F#(最初从OCaml演变而来)中,您可以使用度量单位.设计这个特征的Andrew Kenned(并且还创建了一个非常有趣的理论)有很多系列文章可以证明这一点.
这很可能会在您的场景中使用 - 尽管我不完全理解这个问题.例如,您可以声明两个单位类型,如下所示:
[<Measure>] type litre
[<Measure>] type gallon
添加升和加仑会给出编译时错误:
1.0<litre> + 1.0<gallon> // Error!
F#不会自动在不同单位之间插入转换,但您可以编写转换函数:
let toLitres gal = gal * 3.78541178<litre/gallon>
1.0<litre> + (toLitres 1.0<gallon>)
关于F#中的度量单位的美妙之处在于它们是自动推断的,并且函数是通用的.如果你乘以1.0<gallon> * 1.0<gallon>,结果是1.0<gallon^2>.
人们已经将这个功能用于各种事物 - 从虚拟仪表的转换到屏幕像素(在太阳系模拟中)到转换货币(金融系统中的美元).虽然我不是专家,但您很可能也会以某种方式将它用于您的问题域.
如果它以不同的基数表示,您只需添加模板参数作为基础.这将区分这些类型.一个float是float是float-如果你不想要两个float值是相同的,如果他们确实有相同的价值,那么你需要告诉类型系统了.