Monthly Archives: November 2013

Practical Dependent Types

This morning I found another practical need for dependent types. The details are confidential, but the situation is a common one so I’m not giving anything away by explaining the general situation.

It’s quite simple: we have an embedded device with a flat fixed “file system”. There are no file names, just 10 fixed-size “slots” where a file can go. Each slot is reserved for a particular module of the program to store its persistent data, and has a binary format that is only useful to that module. For example, slot 3 might hold a configuration for calibrating power module. [1]

So how does the power module read its configuration from the file system? A simple implementation is something like this:


The suspect piece of code is the cast from void* to PowerSystemFile*. I think its generally a code smell to have to cast like this. What may be a clue to the validity of this smell is that if the language were completely type-safe then this cast would be either completely disallowed or it would result in a runtime check (and possibly a runtime failure). And in a language like C/C++, a static cast like this is a potential entry point for catastrophic failure with some very strange symptoms. So the question is, how could this be implemented to not require a cast, so that the compiler can verify that we’re doing the right thing?

This to me is an ideal situation for dependent typing. I’m going to make up a fictitious language that might express the things needed to make this example work the way I want it to.


Let me briefly explain the syntax of the above imaginary language in case it’s not completely self-evident. The struct FileSlot<> take an integer argument. For those who know C# or Java, the syntax should look familiar, except that in this case FileSlot doesn’t take a type parameter but an “enum” parameter. The switch statement effectively creates a tagged union.. depending on the value of id (the tag), a different member of the union will be accessible. In this case though, the tag is not part of the union structure, rather it is passed in as a type parameter.

The especially interesting piece of code is the declaration of get_file_data, which returns a FileSlot<id> which is a type dependent on the parameter value id. This is really the dependent type, since it’s the first time we’re saying that the parameter of FileSlot can be a variable.

For the sake of comparison, I’m going to implement this in C++ as well:


The first thing I’d like to point out is that you can actually do this in C++. But there are some important differences. The most practical difference in my mind is that the C++ version is purely a compile-time concept. The id is not a parameter of get_file_data, it’s a template parameter that is used to instantiate an instance of get_file_data for each id that it’s used with. If you only knew the id at runtime then this function wouldn’t work at all (for example if you needed a function that loops through all the files to do file synchronization).

In my hypothetical language the FileID id parameter (of both the type and the function) is a real runtime variable. In the case where the id is constant, the compiler could choose to do a constant propagation optimization to emit exactly the same binary as the C++ version, so I don’t see this as a compromise on performance. On the other hand the compiler could keep the runtime version if it was actually more efficient – which in this case it probably is since our model has a flat file structure where get_file_data probably just fetches data from the id location in the file medium.

As a final note, I don’t actually like any of these solutions completely. The reason is code cohesion. This example requires that we define all possible values of FileID in one place (the enum declaration), and correspondingly all possible types (or template specializations) of FileSlot need to be defined in one place (although they may be physically separated by using #include, the coupling is still there). This has some benefits (if you need to know all the file types then you know where to look), but it smells to me because of its lack of modularity. This isn’t a downfall of dependent types, it’s just a downfall of this particular design.

Anyway, I hope that by giving you a practical example of where a dependent type may be useful that I’ve set off a spark in your mind. And I hope I’ve made you feel a little bit more uncomfortable in your most used language, like I am every day. Enjoy the bitter taste now that you can taste it, because without it you wouldn’t know to move to fresher pastures. [2]

[1] This whole example is completely inaccurate relative to the real situation, but it works well as a simplified model that explains the essence of what the requirement is.

[2] If you can’t taste it, don’t worry. Just wait 10 or 20 years and you’ll be jostled along with the rest of the herd.

The speed of C

Plenty of people say C is fast [1][2]. I think C is faster than other languages in the same way that a shopping cart is safer than a Ferrari.

Yes, a shopping cart is safer.

… but it’s because it makes it so hard to do anything dangerous in it, not because it’s inherently safe.

I wouldn’t feel comfortable in my shopping cart rattling around a Ferrari race track at 150 mph, because I’d be acutely aware of how fast the tarmac is blazing past my feet and how inadequate my tools are to handle things that might go wrong. I would probably feel the same way if I could step through the inner workings of a moderate Python program through the lens of C decompiler.

To put it another way: almost everything that makes a program in language XYZ slower than one in C probably uses a feature which could you could have synthesized manually in C (as a design pattern instead of a language feature), but that you chose not to simply because it would have taken you painfully long to do so.

I bet that you could probably write C-like code in almost any language, and it would probably run at least as fast (with a reasonable optimizer). You could also drive a Ferrari as slow as a shopping cart and it would be at least as safe. But why would you?

[1] 299 792 458 m/s
[2] the_unreasonable_effectiveness_of_c.html

Programming with no rules

A type system in a programming language provides rules and restrictions. They tell you all sorts of things that you can’t do. Ever find yourself jumping through hoops just to satisfy the compiler’s stupid rules? It’s even worse with functional programming, where you can never change the value of a variable after “setting” it. What’s the point of rules except to get in the way?

They give you a path:

When driving to work, you don’t complain that you’re restricted to drive only on the roads. Driving down the road makes easier to navigate. If you were to drive arbitrarily through gardens and parks and shopping malls, apart from wrecking your car you would also find it much harder to navigate. Normally you only have to consider which way to turn when you get to a junction, but now everywhere is a junction! Everywhere is a new choice.

They make it easy:

If society were to abandon roads because they restrict your driving too much, then where would we put the tar to make driving more pleasant? In other words, the more restricted we are about what we’re allowed to do, the better we can work on and improve those few things that we allow.

There are two points to this. The one is that if you have tons of options at each decision in making a program, then to describe one of those options is more difficult. This is simple information theory: the more “expected” something is, the easier it is to represent. The less information you need to convey, the easier it is to say it.

The other point is simply related to the work involved in giving you all the options. It’s easier to make road-cars and roads than to either make all cars capable of driving over anything, or to simply tar everywhere. In other words it takes time and money to implement language features, and time and effort to learn to use them. Although it’s theoretically possible to just tar everything, the resources involved would better be spent on making the existing roads more pleasant and safe to drive on.

They come with some guarantees

The rule that people must drive on the road comes with some great advantages that we all know and love. For example, I don’t need to do my gardening with the expectation that people might drive through it [1]. I don’t need to wear a helmet in the mall. If I better know what to expect from the behavior of a car, then it makes it easier to plan my own behavior and easier to do things in general.

In other words, even though rules can restrict one entity, they really help when it comes to cooperation between multiple entities. And cooperation is the key to making big programs. I’m not talking about cooperation between programmers, I’m talking about cooperation between parts of a program. The more well defined the rules of the game (language and interface specifications), the more the players can play instead of worrying about what others do or don’t do.

If I had to program with no rules, it would only be easy for the very first piece of code. The second piece I would now have my first unruly piece of unpredictable code to interact with, and so I’d have to put on a helmet and tons of error checking.

But what if we just have the best of both worlds? What if we say there are just “guidelines” – you get all the benefits of the rules, except you can bypass them in the case where you have good reason to do so?

Just guidelines

Sounds like a good idea [2]. Now you can drive on the road most of the time, because it’ll give you all the benefits of the rules, but you can turn into a park if you need to get to the other side and it’s too far to go around. We advise you not to cast an int to a std::string, but the referee won’t blow the whistle if you decide that’s what you want [3] [4].

But wait, what about me? Do I need to wear a helmet when I’m potting my pretty petunias or not? I’d better call up every single person who lives in the area to see if they plan on driving today.

In short, guidelines are stupid when it comes to cultivating cooperation [5]. There should be a well-defined set of rules, which the compiler/referee/traffic officer will enforce, that tell you exactly what behavior you can expect from another part of the program. If a function has a return type of a string, you should be damn sure it’s not returning an integer, otherwise there’s no point in playing anymore and I give up!

Public Safety

The metaphors intersect when it comes to security and safety critical applications. The traffic lights are running software, the ATM is running software, paypal is running software, the x-ray machine is running software. In a C/C++ world, where there are only guidelines, and where you can make a call to a string instead of a function, and free a banana instead of a pointer, there is no such thing as guaranteed security. C programs can’t even guarantee that they won’t do something terrible when there isn’t malicious intent. Keeping your password as a “private” unused field doesn’t mean it can’t accidentally be sent to mars, and keeping it “const” doesn’t mean it can’t accidentally be changed. Not assigning to the x-ray-strength variable doesn’t mean it won’t change “on its own” because of some crazy pointer mistake in an unrelated part of the system. No piece of C/C++ code comes with any guarantees when it’s integrated with other code. Instead of commenting functions with what they do, they should all be commented with “this function really does anything, but what I hope it does most of the time is this…”


I do exaggerate a little [6]. But the point is clear: rules offer more advantages than guidelines when it comes to making and interacting with predictable software. Because of its roots in math, software is one of the few (perhaps the only) engineering disciplines where it’s actually possible to completely and perfectly guarantee behavior. And it’s even easier to guarantee the lack of certain unwanted behaviors (eg using strings as integers, or accessing memory you don’t permission to). This is not a “guarantee” in the legal sense, where you get your money back if it’s wrong. This is a guarantee in the mathematical sense, where there is no such thing as wrong. I think we need to use this to our advantage. Seriously.

To anyone who feels comfortable in C or C++ I say, you need to set your standards higher! There is another world on the other side where there is no such thing as segfault or a heap corruption! There is a place where you can tell what a function doesn’t do just by looking at it’s signature! Come and join me!

[1] I don’t actually have a garden. What a shame

[2] Sure, I’ll play along

[3] string s = (string&)x

[4] It’s ok, because I’ll remember to only call it with an int that’s actually a string so I won’t kill any puppies

[5] Guidelines are still good for communication between cooperating individuals, but they can’t be trusted like rules can

[6] Just a little