F#/在编译时验证数组长度的最简单方法

Question

我有一些科学项目。那里有各种长度的向量/方阵。显然(例如)长度为 2 的向量不能添加到长度为 3 的向量中(依此类推)。有几个 NET 库，它们处理向量/矩阵。它们要么都有通用向量/矩阵，要么有一些非常特定的向量/矩阵，它们不适合需求。

这些库中的大多数(如果不是全部)都可以从列表或数组创建向量。不幸的是，如果我错误地输入了错误长度的数组，那么我将得到一个错误长度的向量，然后一切都会在运行时崩溃!

我想知道是否可以在编译时检查数组长度，以便在假设我尝试将 5 元素数组传递给长度为 2 的向量“构造函数”时出现编译错误。毕竟，printfn 几乎做到了!

我想到了 F# 类型提供程序，但我不确定如何在此处应用它们。

非常感谢!

Answer 1

感谢 OP 提出一个有趣的问题。我的回答频率下降不是因为不愿意提供帮助，而是因为有几个问题引起了我的兴趣。

我们在 F# 中没有依赖类型，并且 F# 不支持带有数字类型参数的泛型(如 C++)。

但是，我们可以为不同的维度创建不同的类型，例如 Dim1、Dim2 等，并将它们作为类型参数提供。

这将允许我们为 apply 提供一个类型签名，该签名将向量应用于如下矩阵:

let apply (m : Matrix<'R, 'C>) (v : Vector<'C>) : Vector<'R> = …

除非矩阵的列与向量的长度匹配，否则代码不会编译。此外;结果向量的长度为列的行数。

一种方法是定义一个接口(interface)IDimension和一些代表不同维度的具体实现。

type IDimension =
  interface 
    abstract Size : int
  end

type Dim1 () = class interface IDimension with member x.Size = 1 end end
type Dim2 () = class interface IDimension with member x.Size = 2 end end

向量和矩阵可以这样实现

type Vector<'Dim  when  'Dim :> IDimension 
                  and   'Dim : (new : unit -> 'Dim)
           > () =
  class
    let dim = new 'Dim()

    let vs  = Array.zeroCreate<float> dim.Size

    member x.Dim    = dim
    member x.Values = vs
  end

type Matrix<'RowDim, 'ColumnDim when  'RowDim :> IDimension 
                                and   'RowDim : (new : unit -> 'RowDim) 
                                and   'ColumnDim :> IDimension 
                                and   'ColumnDim : (new : unit -> 'ColumnDim)
           > () =
  class
    let rowDim    = new 'RowDim()
    let columnDim = new 'ColumnDim()

    let vs  = Array.zeroCreate<float> (rowDim.Size*columnDim.Size)

    member x.RowDim     = rowDim
    member x.ColumnDim  = columnDim
    member x.Values     = vs
  end

最后这让我们可以写出这样的代码:

let m76 = Matrix<Dim7, Dim6> ()
let v6  = Vector<Dim6> ()
let v7  = apply m76 v6 // Vector<Dim7>

// Doesn't compile because v7 has the wrong dimension
let vv = apply m76 v7

如果您需要广泛的维度(因为您有一个代数递增/递减向量/矩阵的维度)，您可以使用教堂数字的一些智能变体来支持它。

这是否可用完全取决于我认为的读者。

PS。

如果度量单位应用于比 float 更多的类型，也许也可以用于此目的。