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:

- Add the actual element to the front of the list
- Update the length
*value*by adding 1 - 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.

Hello Kurt,

ReplyDeletePretty neat. Definitely more readable than having the length parameter expand to Succ Succ Zero and so on.

I haven't looked at units of measure yet so i'm not quite clear on what the cons function is doing. How does the unit of measure increase to ^2 and so on?

Can you use units of measure with other types besides float?

>>

ReplyDeleteI haven't looked at units of measure yet so i'm not quite clear on what the cons function is doing. How does the unit of measure increase to ^2 and so on?

<<

The trick is in the multiplication, and the fact that the F# compiler is smart enough to know that unit length * length has unit length^2. So the cons function just multiplies with unit length every time a new element is added, and the exponent increases accordingly.

It would be straightforward to make a 'tail' function that divides by length, which would decrease the exponent.

When adding two unit-typed values, the compiler checks that the units are the same. This is what results in a type error if the lists are of unequal length.

I recommend Andrew Kennedy's blog for a more elaborate explanation - the link is in the post.

>>

Can you use units of measure with other types besides float?

<<

Not natively I think, but you can define your own types, as I've done above with the SVec type.