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

Question

I have some scientific project. There are vectors / square matrices of various lengths there. Obviously (for example) a vector of length 2 cannot be added to a vector of length 3 (and so on and so forth). There are several NET libraries, which deal with vectors / matrices. All of them either have generic vectors / matrices OR have some very specific vectors / matrices, which do not suite the needs.

Most, if not all, of these libraries can create a vector from a list or array. Unfortunately, If I mistakenly give an input array of the wrong length, then I will get a vector of the wrong length and then everything will blow up at run time!

I wonder if it is possible to check array length at compile time so that to get a compile error if, let’s say, I try to pass a 5-element array to a vector of length 2 “constructor”. After all, printfn does almost that!

F# type providers come to mind, but I am not sure how to apply them here.

Thanks a lot!

Answer 1

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.