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

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

但是我们可以为不同的维度创建不同的类型,比如 Dim1 , Dim2 以此类推,并将它们作为类型参数提供。

这将允许我们为 apply 将向量应用于如下矩阵:

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

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

如果你需要一个大范围的维度(因为你有一个代数增加/减少向量/矩阵的维度),你可以使用一些聪明的教会数字变量来支持。

这是否有用完全取决于读者。

附言。

你要找的东西的总称是 dependent types

我见过 an experiment 在使用类型提供程序来模拟依赖类型的一种特定风格(约束基元类型的域)时,我不希望使用当前形式的类型提供程序来实现所需的功能。他们似乎太异想天开了。

打印格式字符串看起来是这样做的(事实上,打印机是一个“Hello World”应用程序,用于依赖类型),但实际上它们是工作的,因为它们得到编译器的特殊处理,而且这种机制是不可扩展的。

您注定要在运行时确保正确的长度。

@Justanothermetaprogrammer的评论可以作为答案。下面是它在实际示例中的工作方式。示例中的矩阵实现基于 MathNet.Numerics.LinearAlgebra :

open MathNet.Numerics.LinearAlgebra

type RealMatrix2x2 = 
    | RealMatrix2x2 of Matrix<double>

    static member private createInternal (a : #seq<#seq<double>>) = 
        matrix a |> RealMatrix2x2

    static member create
        (
            (a11, a12),
            (a21, a22)
        ) = 
        RealMatrix2x2.createInternal 
            [| 
                [| a11; a12|]
                [| a21; a22|]
            |]


let m2 = 
        (
            (1., 2.),
            (3., 4.)
        )
        |> RealMatrix2x2.create

#seq<#seq<double>> 可以很容易地生成代码使用,例如,Excel或任何其他方便的工具,为许多方面的需要。事实上,整个类连同任何其他必要的运算符重写(如 RealMatrix2x2 通过 实矩阵x2x2 ,…)可以为所有必需的维度生成代码。