Fun with units of measure

Since the CTP, F# has a nice feature in its type system, called units of measure. Briefly, it allows you to specify a unit with any float, and the type system checks that your uses of units are consistent. For example, you can't add a float<m> to a float<ft>, which results in, among other things, less crashes of spacecraft on Mars. I won't go into details, if you're interested but don't know what I'm talking about, read Andrew Kennedy's blog before you continue.

But anyway, using units for, well, tracking units is kind of boring - type systems are made to be abused after all. So here's my attempt to use units of measure to track the lengths of vectors, so that the compiler will for example detect that you try to add two vectors of unequal length.

How can this be achieved? The basic idea is to encode the length of the vector as an exponent to a unit, that is kept in the 'safe vector' type as a unit of measure parameter. To do this, we first need a unit of measure and a 'safe vector' type that uses it:

[<Measure>] type length

type SVec<'a,[<Measure>]'l> = 
    SVec of list<'a> * float<'l>

 

So, SVec is a vector containing elements of type 'a, and with a length encoded in 'l. We'll use the float to both encode the length of the string as a value and as a type; the idea is that SVec ([1,5], 2.0) has type SVec<int, length ^2>. Let's define some utility functions to make type safe vectors:

let nil = SVec ([],0.0)
let cons elem (SVec (xs,un:float<'l>)) : SVec<_,'l length> = 
        SVec (elem::xs, (un + 1.0<_>) * 1.0<length>)
let (=+=) = cons

let removeUnits f = f |> box |> unbox<float> 

let length (SVec (_,c)) = removeUnits c |> int 
let from_list xs (l:float<'u>) : SVec<'a,'u> = 
    if List.length xs <> int (removeUnits l) then raise <| new ArgumentException("Actual length of list is not equal to given length")
    else SVec (xs,l)

'nil' constructs an empty vector. It has type SVec<'a>,1>, denoting a list with zero elements. 'cons' adds an element to the front of the vector. To do this, it needs to do three things:

1. Add the actual element to the front of the list
2. Update the length  value by adding 1
3. Update the length type by multiplying with 1.0<length>

To get the length of a vector, we return the unit value, stripping of all static unit types. I tried this first by dividing by 1.0<'u>,  but it appears that you can't use a type argument as a unit of measure with a constant value. I'm not exactly sure why.

'from_list' takes a list and turns it into a safe vector. You need to provide a list, with the length of the list correctly encoded in both value and type. The value is tested, the type is not: as far as I can see, this is impossible to check.

Let's make a safe vector:

let l = 3 =+= (2 =+= (1 =+= nil))

The type of l is SVec<int,length^3>. Now we can define type-safe multiplication and addition:

type SVec<'a,[<Measure>]'l> = 
    SVec of list<'a> * float<'l>
        static member (+) (SVec (xs, l1): SVec<_,'l>, SVec (ys, l2): SVec<_,'l>) = 
            SVec (zip xs ys |> map (fun (x,y) -> x + y), l1)
        static member (*) (SVec (xs, l1) : SVec<_,'l>, SVec (ys, l2): SVec<_,'l>)=
            zip xs ys |> sum_by (fun (x,y) -> x*y)    

The interesting part is of course not the implementation, but the types: they statically enforce that when you add or multiply two vectors, they have the same length. So:

let sum = l + l

will typecheck fine, but

let badsum = l + nil

will give a type error!

That concludes my experiment. Some final thoughts:

• This cannot be used to make a type safe head and tail operation, as far as I can see. We'd need an additional type to represent the empty list, and somehow make a head function that can transform between the two types - the kind of overloading necessary does not seem to be possible in F#.
• Try to make a recursive function  with SVec: it's impossible, since generic recursion is impossible.

Technorati: F#,units of measure