Dependent Types (in Swift) Save the World!

Dependent Types, sometimes referred to as Constrained Types make code safer and easier to work with. Using Dependent Types is one of the most useful and least known programming concepts out there. I hope that after you read this you’ll feel like a mechanic who just learned how to machine their own parts.

I’ll give a little background, then show you how Dependent Types can save the world.

What is a Dependent Type?

In computer science and logic, a dependent type is a type whose definition depends on a value. A “pair of integers” is a type. A “pair of integers where the second is greater than the first” is a dependent type because of the dependence on the value. — wikipedia article on Dependent Types

Since there is little distinction between primitive and user types in Swift, there’s a good chance that you’ve already used a dependent type.

Consider the unsigned integer type: UInt¹

UInt(exactly: 1)   // 1
UInt(exactly: 1.0) // 1
UInt(exactly: -1) // nil

Whether or not you’re able to create a UInt is dependent on
a) the value that you pass to the initializer being positive and
b) the value being resolvable to a whole number

When you use a UInt you’re conveying the information that you’re dealing with a positive whole number. This is helpful.

Time to Save the World!

Let’s imagine our job is writing software for a nuclear power plant.²

If the reactor overheats it could trigger a climate event and lead to the end of life on Earth. We need a function to cool it:

func addCoolantToNuclearPowerPlant(gallons: Int)

Potentially you could call this with a negative number:

func doEmergencyStuff() {
    addCoolantToNuclearPowerPlant(gallons: -1000000)
}

You’ve just drained all the water and triggered a nuclear catastrophe. It is easy to see why the type UInt would be a safer choice for this parameter.

func addCoolantToNuclearPowerPlant(gallons: UInt)

Now let’s say the power plant requires a minimum of ten thousand gallons of coolant when it overheats. In our current definition, we cannot drain the coolant by accident (whew) but we can still pass an insufficient amount of stuff to our cooling function. Let’s fix this by adding a check within the function so that we don’t overhead the reactor by accident.

You’ll notice from the check that there is an implicit dependency on the value of the parameter.

We can and should make the implicit explicit by defining a new Dependent Type. Let’s call it Coolant.

This definition of Coolant uses a fail-able initializer to ensure that it cannot exist unless there are at least ten thousand somethings of Coolant. Now we can redefine our cooling function as follows.

It is now impossible to invoke this function with anything but the minimum amount of Coolant needed.

Quick Recap:

1. We recognized that the cooling function took a value that had a an implicit requirement. We could tell that it had a requirement because the function was checking the value before using it.

2. We moved that implicit requirement into a new type that could only be created with a value that explicitly satisfied the requirement

3. We used that new type in our cooling function, thereby moving the logic out of our function and into the type of the parameter that the function takes

Okay, back to saving the world.

Inventory Issues:

Our current solution has a problem. Think about the inventory system that handles the supply of coolant. Imagine how a naive implementation might look.

It would be easy to do something like:

if !inventory.coolantSupply.isEmpty { ... }

This could lead to a nuclear meltdown. Having a supply of Coolant does not mean that you actually have Coolant.

We need to change our definition of Coolant to not be fail-able. Let’s do this by defining another dependent type, AtLeastTenThousand to represent a number that is at least 10,000.

Using this we can redefine Coolant to take a parameter of AtLeastTenThousand. This makes it easier to use but more importantly it moves the fail-able aspect down a level. Out of the initializer for Coolant and into a Dependent Type that Coolant relies on.

Quick Recap:

There was a problem with managing the inventory of Coolant due to its optional nature. We solved this by taking the following steps to make it non-optional.

1. Recognized that the initializer for our Dependent Type Coolant took a value that had a an implicit requirement. We could tell that it had a requirement because the initializer was checking the value before using it.

2. We moved that implicit requirement into a new Dependent Type, AtLeastTenThousand that could only be created with a value that explicitly satisfied the requirement

3. We used that new type in the initializer, thereby moving the logic out of Coolant's initializer and into the type of the parameter that the initializer takes

Is this Overkill?

Imagine the nuclear power plant has a failsafe in case the inventory supply is unavailable. They’ve asked us to write a standalone function that can run if somebody pushes the proverbial red button.

This emergency function will still have to guard that the input to Coolant is valid.

In this case it’s easy to overlook the benefit of having a Dependent Type for Coolant. In a small example you’re probably right, it’s probably overkill. We could just as easily have written:

The reason the first is better is that in the real world you’re likely working in a large application where you have hundreds of classes, where you have to remember to do logic and safety checks and keep the requirements of particular types in your head while refactoring and then somebody interrupts you to ask a question and your phone rings etc etc… The less brain power you can devote to low-level requirements the more time and energy you can put towards solving difficult problems.

Adding Requirement to a Dependent Type:

So this is not bad but we did miss one thing. Our function is misleading. It says it accepts gallons but nothing in Coolant enforces this implied requirement. Let’s rewrite Coolant to enforce this requirement using Foundation’s Measurement type.

This is better since our code will now handle unit conversion correctly. However we’ve ‘broken’ Coolant by making it fail-able. Once again we can clean this up by using a dependent type. Let’s call it Gallon.

Now we can refactor Coolant to once again be non-fail-able:

Quick Recap:

There was a potential issue with using Coolant due to its lack of clarity around measurement units. We solved this by taking the following steps to ensure that Coolant can only be created with the correct measurement type.

1. Recognized that the initializer for our Dependent Type Coolant took a value, UnitVolume that had a an implicit requirement. We could tell that it had a requirement because the initializer was checking the value before using it.

2. We moved that implicit requirement into a new Dependent Type, Gallon that could only be created with a value that explicitly satisfied the requirement

3. We used that new type in the initializer, thereby moving the logic out of Coolant's initializer and into the type of the parameter that the initializer takes

One last thing:

We can clean up our standalone emergency function even more by changing the stored value of AtLeastTenThousand to be a Double. We can safely use a Double even though a Double can be negative because this particular Double will never be negative.

Coolant should look like this now:

It’s a small change but having to cast to a Double at the point of use is ugly. Why not move one more piece of information to our Dependent Type?

Now when you go to use Coolant in a function you have assurance that you’re using enough of it and that it will use the correct units.

Testing Dependent Types:

I haven’t mentioned testing until now because there are a lot of articles out there on testing basic classes and structs and that’s basically all these are.

I should mention that this is one of the joys of these types. If you have a thoroughly tested implementation of AtLeastTenThousand, and Gallons, then you don’t need to test Coolant because there is no logic in it all.

Conclusion:

I think this quote summarizes the appeal of Dependent Types for me.

Dependent types reduce certification to type checking, hence they provide a means to convince others that the assertions we make about our programs are correct. Dependently typed programs are, by their nature, proof carrying code

— Thorsten Altenkirch, Conor McBride, and James McKinna: Why Dependent Types Matter. April 2005

This is it in a nutshell. It moves Type Safety into the lowest level you possibly can.

You may have noticed that we were following a pretty clear pattern throughout this process.

1. Notice that a value has a requirement (greater than, less than, is a, contains, etc…) by the way it is used
2. Move that requirement down a level into a new type that can only be created if the value matches the requirement
3. Use that new Dependent Type in place of the old value
4. Repeat until everything is as small and trusted as possible

So the next time your nuclear reactor is overheating, you can trust that your code will work to cool it down.

Or you could just throw water on it.

Thanks for reading!!!

[1] I realize that UInt is actually more of a convenience wrapper that Swift provides for accessing UInt8 or UInt16 et al so that you don’t have to pay as much attention to memory management. It may be a stretch to call it a dependent type but it helps me illustrate an example.

[2] I am not a nuclear engineer. If anyone who knows a lot about nuclear power plants reads this; I am so sorry.