## Building (Almost) Dependent Types in Swift

Dependent typing is something most of us use in a restricted form, but that most working programmers don’t really encounter in its “stronger” forms outside of school. Parametric polymorphism is the most common expression of type dependence, which lets us have functions or other types that are dependent on the types of either parameters or a type parameter to the class itself. This is mostly commonly called generics in most languages, and permit us to generalize the way we write code so that we can use the same algorithm even though the types may vary - the classic example being an array or vector.

There’s another side to dependent typing though that gives us even more freedom, and the best way to introduce it is to ask a simple question: what about tuples? While languages like Swift have built-in tuple types, what type is a tuple really? Is it a type that is parametrically polymorphic as we noted above? Sort of - we know that it should store any arbitrary data type, but the difference between a 3-tuple and a 4-tuple is not the same as the difference between a list containing three items and a list containing four items - indeed, a 3-tuple and a 4-tuple are separate types. The n-tuple is a dependent type based on a value - the number of elements it contains. This is where we really get the value out of dependent typing - we can define functions that only operate on 4-tuples, or functions that only operate on 8-tuples, and then enforce this at compile time using Swift’s static type checking. This helps us stop misuse of functions and methods before runtime, and helps us keep bugs out of our code.

So, let’s dig in, after all, why should Apple get to have all the fun with their tuples?

### Tuple Typing

Let’s have a look at some code and how it evaluates in Swift to convince ourselves that tuples work this way. One thing to note, throughout this post I’m going to be using the reflect function in Swift, which lets us get a MirrorType for any object, letting us get easy access to its actual type and other information.

If you try this for yourself, you can see that we get a statement of “false” printed. The types in question are shown as (Int,Int,Int).Type and (Int,Int,Int,Int).Type. We can see here that not only does the type of the values stored determine the type of the tuple, but as we said, so does the number of elements. This makes it clear that there is at least one very common case where allowing dependent types based on values not just types would be valuable. With this in mind, let’s see if we can implement “pseudo” dependent types in Swift with the end goal of implementing a type system rich enough for the tuple type ourselves.

## Building (Almost) Dependent Types

Before we can tackle tuples, first we have to figure out how to represent a value in a type. For now, let’s talk about the type we’re going to generate for a particular value in terms of a type constructor, $$F(x)$$ where $$x$$ can vary over our input domain of valid values for our dependent type system. Given this type constructor, it must satisfy a few fairly common sense properties for us to be able to use it for dependent typing.

The first property is that the function must always map a given input value to a given output type - that is, the type generated for a given input must remain the same and compare as equal regardless of how many times we call the type constructor. Another way to state this is that we have to guarantee that $$F(x)$$ is a pure function, that is, it causes no observable side effects, and relies on no external state.

The second property is that for two given inputs to the type constructor, the output must be unique. To state this mathematically the function must satisfy the following rule $$\forall x_{0},x_{1} \in X, x_{0} \neq x_{1} \implies F(x_{0}) \neq F(x_{1})$$. This guarantees us that our function is a one to one map for values to types.

### Recursive Type Representations in Swift

Swift is great because it offers very good static type checking - but this also present us with a bit of a problem as we try to generate dependent types. To build our types, we have to rely on values that are not known until runtime, but to build the types, we have to construct a type based on the arbitrary input. This puts us in hot water, as it means that the type inference system cannot figure out our types, and in fact, it’s not even entirely clear how we can do this in Swift’s syntax.

To solve this, let’s think about what the types we have will actually represent. For now, for the purposes of simplification, let’s limit the values we support to positive integers, that is we’ll limit the domain $$X$$ of our function to be the set of positive integers supported in Swift. This makes sense since it’s all we need for tuples, but we can also generalize this approach as we’ll discuss later. Based on this, the type we generate with our function really just needs to be an encoding of the type itself. Swift offers us generics, so what if we used container types, and string them together in such a way that they represent the values. Let’s look at a few examples.

Based on the above, it’s fairly clear that this also satisfies the properties we mentioned before - for any input, the type it generates will be unique, and for any input the type will always we the same. Now that we have a method of representation, we just have to write our actual type constructor.

### Generating (Almost) Dependent Types

As it turns out, we can use a recursive function to actually generate the type we want. The only problem we will run into with this sort of setup is how we actually pass the type up the stack in such a way as to not confuse the type inference engine. We can do this using an accumulator, given that this is a recursive function, which also has the useful side effect of making this function tail recursive. We use MirrorType here at the top as a convenience to avoid some weird casting.

So we can see here that we have a wrapper function called valueTypeForValue that takes an integer and then returns a type by simply calling the recursive call and unwrapping the result from the MirrorType.

The recursive function itself takes what is in the accumulator, embeds it in a ValueTypeTerm as the parametric type, and then recursively calls itself until it hits zero. Once zero is reached, it wraps it in a MirrorType, and returns the result.

If we do some testing in a playground, we will quickly find that this does exactly what we want: it generates the types exactly as we specified in our previous representation. The returned types also meet the two requirements we stated originally.

There’s one problem we haven’t solved yet though: we can now represent types with numeric values, but another aspect of dependent typing is that the value type may actually change the semantics of the type itself. In other words, a tuple is dependent not just on the number of elements it has, but also the type of those elements. So it looks like we’ve moved the goal now that we’ve reached it, so let’s dig back in.

## Back to the Drawing Board…

There’s a few directions we can head from here - but the most obvious is probably to extend our type constructor to not only be dependent on the integer, but also on a set of types themselves. In other words, instead of just passing in an integer, you would also pass in a list of types that dictate the order of the Tuple. This makes some intuitive sense, but first we have to think about how to tweak our model and see if it makes sense.

Previously, we used a model where we nested types - we will still need to use this model to represent the integer portion of our type, but we also want to represent the type of a given tuple index. Why not just add another parametric type to our container, use one of them to handle the nesting, and use one of them to handle the type for the index of the current type. Let’s look at a few examples quickly.

This is pretty simple - we’re just adding a parametric type value alongside the “depth” to indicate what type is available at each depth. This sounds like it will work.

### Modifying Our type constructor

Given our modified representation, now we just have to modify our type constructor to generate our types. The obvious way to do this would be to let someone pass in the types themselves - but doing so you end up running into issues with the type inference system. Our entire strategy around using the type system revolves around us being able to build a type up dynamically to represent our structure, and when we pass in the types we cannot create this structure dynamically since Swift is statically typed and we cannot reference types in this way at runtime.

Instead, we can pass in the actual values themselves, and construct our structure based on the objects, with their rich type information, but there’s still another problem here: if we accept [Any] the objects lose their type information as well. We also cannot dynamically cast based on an Any.Type or we could pass in MirrorType objects and cast their values to their valueType. Well, that puts us in a bad position, but there is one option: we can recursively, and in a quite ugly way, generate our tuple type based on the types we want to pass in.

Let’s have a look at the very simple code that accomplishes this, then we can talk more about it.

We can see that this recursive building function basically has us pass in a value at each step, combined with a container structure. The function then aggregates the container structure with the value passed in. At the base case, we have a container that has any types in it to mark that we are done. Here you can see we create two tuples, one of what we would call type (Int, String, [Int], Int) (not literally this type in Swift, but what you can conceptually think of as representing this type) and one of what we would call type (Int, String, [Int], [Int]). If we use reflect and valueType to get their types, we can then actually compare the types and see that they are actually fundamentally different.

This is very ugly, and there are ways we could potentially clean it up, but it’s difficult as we run into a lot of problems where Swift won’t let us change things so it can preserve its static typing capability - which ironically is part of what really gives us value in these sort of approaches.

## Generalizing This

With what we’ve done, we are capable of representing and even implementing a tuple using dependent typing. We can extend this to other arbitrary classes of values as well as types using multiple techniques, but they all come down to the primitive operations we displayed here: recursively building types and using polymorphic types to represent dependent types. Regardless, it’s important to note we still haven’t given the type system truly dependent types - just provided a workaround to let us pretend it does in some cases.

## Conclusion

After discussing why dependent types are important, we have managed to build pseudo-dependent types based on values in in Swift. These types, while not truly giving us a dependent type system, prove that Swift is rich enough that it’s even possible to (almost) extend the type system itself if you’re willing to jump through enough hoops. I wouldn’t recommend using the final results here in most cases, but in some cases, using value driven dependent typing, even when the implementation itself is ugly, can lead to much cleaner and safer results.

I hope you’ve enjoyed the post - as always, please feel free to let me know of any errors I’ve made or any improvements you think I could make to the article. I’ve done my best to keep it accurate, but I’m quite fallible.

Oh - one last note - for those of you that are research computer scientists or theoretical purists, I’ve stepped on type theory quite a bit today without getting into any real depth in terms of explaining how type systems work, why dependent typing matters, the different ranks/types of dependent typing, nor a lot of other very important details. This was done intentionally to keep this article accessible. Rest assured, I’m preparing another article to dig into these topics a lot more though and you’re welcome to nitpick it as much as you’d like!

## Thanks

Thanks to curryhoward from hacker news for pointing out some terminology errors I made and suggesting some other corrections for clarity - as always such corrections are appreciated!

Aug 11th, 2015