What I Learned Approching Idris With An Agenda

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 Int, 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 Color.

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

Now, 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[30], 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

A Vect would look like:

data Vect : Type -> Nat -> Type where
  Nil : Vect a 0
  Cons : a -> Vect a n -> Vect a (n + 1)

Either a 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 xs to xs, not xs to 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

OhmygodlookatthattypeI’mnotwritingfuckingScalaherewtf?

So what was going on here? Why did we have unresolved with blocks and what do Force and Delay mean?

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 Force

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.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s