A few years ago I wrote up a little Scala library for dealing with dimensioned units of measure. This had two implementations.
One was type-safe, but required defining all the combinations of dimensions and the operators to yield them manually.
One was dynamic, determining the dimensions of a given quantity based on the dimensions of the quantities and operator used to combine them.
This was slightly frustrating, as encoding the rules to combine sets of dimensions were easy to define, but not representable in the type system, despite being purely typish concerns. A little investigation highlighted dependent typing as a technology which could help solve this problem.
A few weeks ago, I was working through (the excellent) Seven More Languages In Seven Weeks and got to the Idris section. “Ah!” I thought, “a chance to revisit that problem, solve it properly, and gain a deeper understanding of this technology”.
And so I worked through the examples, implemented Vect, did some proofs, and then took a step back and tried to work out how to do what I wanted to do. Here are some of the things I learned along the way.
What is a dependent type?
A dependent type is a type which depends on values. Well, that’s the definition which is often cited. What does it mean?
Well, we have types which are just types: types like
String and so on. We have types which are parameterised, like
List (well, technically,
List is not a type, but
List Integer and
List String are). And then we have types which are parameterised by values, like
Vect 7 Integer (a list of 7 integers).
In the same way as a regular parameterised type’s type depends on the type of values used to instantiate it, a dependent type’s type depends on the value of values used to instantiate it. How it depends on that is entirely up to the programmer.
For the time being, let’s not think about why we might want to do that, and just see how we can do it, mechanically speaking.
Now, this took me a little while to reason out, because Idris’ documentation isn’t so much a specification as a loose collection of examples. It’s entirely possible that I don’t have the full story here but this is as much as I’ve worked out so far:
In Idris, we can define a value like so:
myAge : Integer myAge = 21
Or like so:
doubleMyMoney = Integer -> Integer doubleMyMoney x = x * 2
Because, of course, a function is a value.
These definitions are easy to parse: first line defines the type of the value, then the second line defines the value. Before the equals is the name and the parameter list, and then after the equals is an expression yielding the value.
It’s notable that we can, in this framework, think of a value like
myAge as a function which takes no arguments: in a pure language, there is no difference between a function which takes no arguments (either because that’s how it’s defined, or because it’s fully applied) and a value. Hold that thought.
We define types using the
data keyword. For now we’ll ignore the compact Haskell ADT syntax for consistency:
data Color : Type where makeColor : Integer -> Integer -> Integer -> Color
Structurally, this looks very similar to how we declare values, only this time we need to
data keyword (to specify that we’re defining a type, not a value) and the
where keyword (because Idris requires algebraic data types be closed, so all the constructors need to be colocated).
On the first line, we specify the type of
Color, which is a
Type. Then, in turn, we specify the constructors of
Color, of which we have one:
makeColor, which is a function which takes 3
Integers and returns a
How does it return a
Color? We just specify that it does. Where’s the implementation? Well, we end up with a fully applied function (
makeColor 3 6 1) and treat it like a data structure, because there’s no difference between those things in a pure functional world.
The parameters don’t need names, just types. We can give them names if we want, but it doesn’t really do anything:
data Color : Type where makeColor : (red : Integer) -> (green: Integer) -> (blue : Integer) -> Color
We can parameterise types by type:
data Box : Type -> Type where box : x -> Box x
This just wraps a type in a box, for no real reason other than a minimal code sample.
Box is a type-level function which takes a type and returns a type, and it has one constructor (
box) which takes a value of any type
T and returns a
Box T. When I say
Box is a type-level function with one parameter, you can also think of it as a type-level data structure with one field, because those are isomorphic concepts.
Here we’re taking the type parameter from the argument, but we can also put in fixed type parameters:
data Box : Type -> Type where emptyStringBox : Box String emptyIntegerBox : Box Integer
Here we have constructors for our
Box type which take no arguments, so they’re values. The important thing to note here is that
Box is of
Type -> Type, so in order to get a type, you need to provide a type. That type can come from the parameters, or it can come from the definition of the constructor, but it needs to come from *somewhere*. We can even do things like:
data Box : Type -> Type where stringBox : Integer -> Box String integerBox : Integer -> Box Integer
This allows us to create values like (
stringBox 17 : Box String) and (
integerBox 44 : Box Integer). These types don’t immediately make sense to me, but then again, they don’t *have* to, and there may well be good reasons to do stuff that looks like this which isn’t obvious without context.
We don’t have to parameterise our types with types, though. We can also parameterise them with values:
data Box : String -> Type where box : (n : String) -> Box n
box "hats" is of type
Box "hats", and you can define a function which will take a box of hats but will reject a box of cheese. Similarly, we could define the following constructor:
data Box : String -> Type where hatBox : Integer -> Box "hats" cheeseBox : Integer -> Box "cheese"
Which would allow us to create both boxes containing zero to many hats, and boxes containing zero to many cheeses, and consider them distinct types.
Note however that we have two choices: either we define the value we’re incorporating into the type on a per-constructor basis, or we take the value we’re incorporating into the type from one of the parameters to the constructor, which means it’s part of the data structure.
This then begs the question as to why we would want to do something like this, instead of just introducing separate Hat and Cheese types and parameterising Box with those.
The answer is: there are things we can do with values that we can’t easily do with types. For example, arithmetic.
What do you get when you concatenate two lists? You get a list.
What do you get when you concatenate a list of 7 items with a list of 12 items? A list of 19 items.
There are a bunch of times that reasoning like that is important. For example, if you’re constructing an id for an SQL database column defined as
varchar, you want to ensure that id fits within that 30 characters. So when you’re constructing it by concatenating an area id with a product id with a unique hash, knowing at compile time that the area id is no more than 2 characters, the product id is no more than 4 characters, and the hash is exactly 24 characters conveys a real benefit.
Defining such a list, commonly named
Vect, is pretty elementary. Whereas a regular list would look like so:
data List : Type -> Type where Nil : List a Cons : a -> List a -> List a
Vect would look like:
data Vect : Type -> Nat -> Type where Nil : Vect a 0 Cons : a -> Vect a n -> Vect a (n + 1)
Vect is empty, in which case it has length 0, or a
Vect is an item followed by another
Vect of the same member type and length
n, in which case the resultant
Vect has length
n + 1.
Nat here means natural number, ie zero and the positive integers. In most tutorials this is represented using the symbols
Z (for zero) and
S (for successor: the successor of a number is that number plus one). So, generally speaking, we’d actually represent Vect like so:
data Vect : Type -> Nat -> Type where Nil : Vect a 0 Cons : a -> Vect a n -> Vect a (n + 1)
This representation is important for the sorts of problems you run into fairly quickly, but that’s beside the point. For now, we’ll just do it. Trust me.
At that point you can define functions on Vect which use those numbers:
add : Vect a m -> Vect a n -> Vect a (m + n) add Nil ys = ys add (Cons x xs) ys = Cons x (add xs ys)
This is the interesting point: we’re doing arithmetic on type parameters. And, if we take a step back, and remember that
(+) is just a function here, that means we can do any functional trasformation on type parameters that we can do on values.
That is, as long as those functional transformations are correct. For example, sometimes we try to do things that turn out to be huge mistakes:
add : Vect a m -> Vect a n -> Vect a (m - n) add Nil ys = ys add (Cons x xs) ys = Cons x (add xs ys)
This fails to compile, because the types don’t align. Just looking at
add  ys for example, if we pass in a
Vect of length 0 and a
Vect of length 5, we’re going to get a
Vect of length 5, not the
Vect of length -5 (a meaningless concept, surely) like the signature states. So it’s caught a bug: our type is not correct.
Now, normally, we won’t define our types incorrectly. But we might define our implementation incorrectly:
add : Vect a m -> Vect a n -> Vect a (m + n) add Nil ys = ys add (Cons x xs) ys = Cons x (add xs xs)
Note that in the second implementation of add, we’re adding
ys. The type system will catch that for us too. So far so good. The slight complication arises when it becomes apparent that the type system doesn’t, strictly speaking, catch errors. It catches statements which it can’t prove are true. For example, this implementation of reverse:
reverse : Vect a m -> Vect a m reverse Nil = Nil reverse (Cons x xs) = add (reverse xs) (Cons x Nil)
This is correct, but it yields a type error:
Vect.idr:11:9:When checking right hand side of Main.reverse with expected type Vect a (S n) Type mismatch between Vect a (n + 1) (Type of add (reverse xs) (Cons x )) and Vect a (S n) (Expected type) Specifically: Type mismatch between plus n 1 and S n
That last section boils down to a type mismatch between
(n + 1) and
(1 + n). This is one of the interesting things about Idris: it has a very pricipled idea of equivalence, which boils down to its handling of equals on regular values (equals is NOT definable in Idris). Two expressions are equal if, and only if, they are structurally identical.
(n + 1) does not equal
(1 + n), even though, of course, we know it does.
This is where Idris’ proof capabilities come into play. We know
(n + 1) == (1 + n), but for our types to work we need to demonstrate that in the language. We’re not just doing some cool math-wankery, we’re solving a real problem in a system which provides real value.
I’m not going to go into detail about how we prove that
(n + 1) == (1 + n) here, because that’s too much of a digression. Suffice it to say it’s actually quite pleasant to do so, but I ended up spending some time learning how to implement proofs before I stumbled across a compelling case for them, and not one that was presented in the intros I’d encountered, just one I found when dabbling and testing my own knowledge.
So, let’s see if we can loop back to the beginning again. I picked up Idris to see if it could solve the problems I had elevating dimension logic to the type system in Scala.
It’s relatively straightforward to build a data structure that represents dimensions, from which new dimensions can be derived. In the Scala implementation, I used maps of strings to integers: those present difficulties in Idris because two trees (which is how maps are implemented) can contain the same set of key-value pairs but not be structurally identical, so instead let’s represent them by a list of dimension-power pairs sorted by dimension. Then, it’s easy to assign dimension to any quantity:
data Dimension : Type where dim : String -> Integer -> Dimension Dimensions : Type Dimensions = List Dimension data Quantity : Type -> Dimensions -> Type where WithDim : a -> (d : Dimensions) -> Quantity a d
On the one hand, that means carrying the dimensions along with the value at runtime, where we really only need it to be a type-level concern: we could quite happily erase dimensions at runtime. But it has other advantages: type checking is made a ton easier because of a useful shortcut. Let’s say we want to implement addition on quantities:
(+) : Num a => Quantity a d -> Quantity a d' -> Quantity a (d + d') (+) (WithDim x d) (WithDim y d') = WithDim (x + y) (d + d')
We don’t need to prove anything about how addition on dimensions works here, because the operation in the implementation is structurally identical to the operation in the type. It could do literally anything (including incoherent things) and we’d still type-check at this level.
This is a very important point. Most of the writings about Idris are from a heavily mathematical perspective, and care about proofs. I don’t care about proofs: I care about encoding useful concepts. The value of a type system, for me, is to make a large program easier to reason about by:
- abrogating responsibility for certain concerns from the developer to automated systems
- annotating meaning to values.
Dependent types add another powerful tool to that toolbox of types.
Of course, we’re not just carrying typish concepts in our values because it makes type-checking easier: we’re doing so because that’s the only means we have of injecting them into the type. Making type checking simpler is just a bonus.
In addition, we may decide in time that, for example, commutativity of multiplication of quantities of integers is important, and at that point we’ll need to provide a proof of commutativity of multiplication of dimensions. If we want to do that, we can!
Well, in principle, at least. I have a sinking suspicion that my choice of representations makes commutativity proofs a little bit complex.
This implementation of dimensions and units-of-measure in Idris is not a lot of code. I’m not going to argue it’s brilliant or idiomatic Idris, and I certainly wouldn’t advocate it as being production-ready, if Idris is itself production-ready for anything. It’s just there to show what sorts of cool things you can do with types in Idris after a very shallow exposure.
There’s one last thing I learned whilst writing this library – one thing not to do. When I started putting it together, I’d find my types were easily understandable:
*> :let speed = 10 # metres / 2 # seconds *> :t speed speed : Dimensioned Double [Dim "metres" 1, Dim "seconds" -1]
But then I started doing more work, defining some additional functionality, a bunch of predefined units and dimensions, and at some point something got quite confused:
*> :let speed = 10 # metres / 2 # seconds *> :t speed speed : Dimensioned Double (with block in Dimension.* (Force (Delay (Force (Delay LT))), 0) "metres" 1  "seconds" -1 )
That was a bit alarming, but when I tried some more complex units it went a touch absurd:
*> Capacitance with block in Dimension.* (Force (Delay (Force (Delay LT))), 2) "amps" 1  "seconds" 1  * inverse (with block in Dimension.* (Force (Delay (Force (Delay LT))), 2) "kilograms" 1  "metres" 1  * inverse (with block in Dimension.* (Force (Delay EQ), 2) "seconds" 1  "seconds" 1 ) * [Dim "metres" 1] * [Dim "seconds" -1] * [Dim "amps" -1]) : List Dimension
So what was going on here? Why did we have unresolved with blocks and what do
Let’s start with the latter: the former is a red herring. Unlike Haskell, Idris is strict by default (where Haskell is lazy).
Delay is how Idris encodes laziness where appropriate, and
Force is how Idris takes a lazy value and makes it strict.
Only trouble is: I managed to break that mechanism with my library. I did it by introducing sensible aliases for all dimension-sets for which I had units. So kilograms had dimension
Mass, amps had dimension
Current, and newtons had dimension
I’d introduced a name disambiguation problem. It took me embarassingly long to solve (a good proportion of which was not realising it could be an error on my part), but I renamed the dimensions of newtons to
Weight and everything was sorted.
Do not name things
Force. Idris does not like that.