F# / Simplest way to validate array length at COMPILE time

Thanks to the OP for an interesting question. My answer frequency has dropped not because of unwillingness to help but rather that there a few questions that tickles my interest.

We don't have dependent types in F# and F# doesn't support generics with numerical type arguments (like C++).

However we could create distinct types for different dimensions like Dim1, Dim2 and so on and provide them as type arguments.

This would allow us to have a type signature for apply that applies a vector a matrix like this:

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

The code won't compile unless the columns of the matrix matches the length of the vector. In addition; the resulting vector has the length that is rows of the columns.

One way to do this is defining an interface IDimension and some concrete implementions representing the different dimensions.

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

The vector and the matrix can then be implemented like this

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

Finally this allows us to write code like this:

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

If you need a wide range of dimensions (because you have an algebra increments/decrements the dimensions of vectors/matrices) you could support that using some smart variant of church numerals.

If this is usable or not is entirely up the reader I think.

PS.

Perhaps unit of measures could have been used for this as well if they applied to more types than floats.

The general term for what you're looking for is dependent types, but F# does not support them.

I've seen an experiment in using type providers to mimic one particular flavor of dependent types (constraining the domain of a primitive type), but I wouldn't expect it to be possible to achieve what you want using type providers in their current form. They seem to be too whimsical for that.

Print format strings appear to be doing that (and in fact printers are a "Hello World" application for dependent types), but actually they work because they get special treatment by the compiler, and the mechanism for that is not extensible.

You're doomed to ensure correct lengths at runtime.

My best bet would be to use structs to encode actual vectors and ensure correctness on the API level that way, map them to arrays at the point where you're interacting with those matrix algebra libraries, then map the results back to structs with ample assertions when done.

The comment from @Justanothermetaprogrammer qualifies as an answer. Here is how it works in the real example. The matrix implementation in the example is based on 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

The tuple signatures and "re-mapping" into #seq<#seq<double>> can be easily code-generated using, for example, Excel or any other convenient tool for as many dimensions as necessary. In fact, the whole class along with any other necessary operator overrides (like multiplication of RealMatrix2x2 by RealMatrix2x2, ...) can be code generated for all necessary dimensions.