## Faking dependent types in Swift

Dependent types are types “that depend on values”. Say you had a function `f`

that took an integer. If you can write that function whereby it returns a value of type `A`

when that integer is even, or a type `B`

if the integer is odd, then you’re working with dependent types. (I think. I’m not sure: if I’ve got it wrong tweet me.)

## Dependent Pretendance

As far as I can tell, this is not possible in Swift. All variables are statically typed, and those types must be found at compile-time. As long as you’re not messing around with casting:

```
struct A {}
struct B {}
func f(i: Int) -> AnyObject {
return i % 2 == 0 ? A() as! AnyObject : B() as! AnyObject
}
```

You won’t be able to manage it.

Now, sum types can give you something that *looks* like dependent types:

```
struct A {}
struct B {}
enum SumType {
case Even(A), Odd(B)
}
func f(i: Int) -> SumType {
return i % 2 == 0 ? .Even(A()) : .Odd(B())
}
```

But that doesn’t fit the description: the thing returned is of type `SumType`

, *not* `A`

or `B`

.

That’s fine, though. As with all of these highfalutin mathematical concepts in programming, you can steal some of the cool and fun *patterns* from your Haskells and Lisps and Idrises and implement them in whatever language you want.

As it happens, implementing this stuff in Swift gets you even *further* away from the formal definition of dependent types. Instead of allowing types to be decided at runtime, you end up forcing even *more* resolution and computation to happen at compile-time. Take “numbers-as-types”, for instance:

```
protocol Nat { init() }
struct Zero : Nat {}
protocol NonZero: Nat { typealias Pred: Nat }
struct Succ<N : Nat> : NonZero { typealias Pred = N }
```

Once you encode some numbers by hand:

```
typealias One = Succ<Zero>
typealias Two = Succ<One>
typealias Three = Succ<Two>
typealias Four = Succ<Three>
typealias Five = Succ<Four>
typealias Six = Succ<Five>
typealias Seven = Succ<Six>
typealias Eight = Succ<Seven>
typealias Nine = Succ<Eight>
```

You get thinking about exactly *how much* computation you can achieve at compile time:

## Sum types, divide types, multiply types

What I wanted, ideally, was some basic “Algebraic data types”. (Today. Today was the day I made the worst pun.) I wanted to be able to add the type `One`

to the type `Two`

and get the type `Three`

. Once you can manage those, multiplication, division and all kinds of silliness are possible. I set myself some rules: all calculations must be performed at compile-time, and all calculations must work with arbitrary values.

I’ve not been able to manage, unfortunately. If someone could figure out how to do it, I would love to hear it. I’ve been stealing ideas from Faking It: Simulating Dependent Types in Haskell mainly.

Here’s the kind of code that made me think it was possible:

The types returned by those two methods are different. This is all to do with that protocol-oriented-programming business: the compiler will try to select the most specialised version of a method to use. So in the example above, since an array can just be indexed backwards, the compiler uses a method that returns a lazy `ReverseRandomAccessCollection`

. However, for the `AnySequence`

, the `reverse`

method has to create a whole new array.

With that in mind, we can make a protocol:

Then, we can extend it, like this:

So far, so good! The compiler will add that method to all types that conform to the `where`

clause. So if there is a concrete type that conforms to `BinaryOp`

:

Only instances where `A`

and `B`

are equal will get the type alias:

But that’s not ideal. We want something that returns `NEQ`

when the types are not the same. Easy enough, right?

But there’s an error: `invalid redeclaration of 'Result'`

. The compiler won’t allow polymorphism with typealiases. It *does* allow polymorphism with properties, though:

```
extension BinaryOp {
var r: EQ { return EQ() }
}
extension BinaryOp where A == B {
var r: NEQ { return NEQ() }
}
```

This is already a less elegant solution than the typealiases, since we’re going to have to initialise things. All of the type information is available at compile-time, though, so I’ve not broken any of my rules.

How about something more complex? Instead of `EQ`

and `NEQ`

, maybe `LT`

, `GT`

, and `EQ`

?

It’s hard to see how it would work. Well, here’s the base case:

Then, any non-zero is bigger than zero:

```
struct LT {}
extension BinaryOp where A == Zero, B : NonZero {
var r: LT { return LT() }
}
struct GT {}
extension BinaryOp where A : NonZero, B == Zero {
var r: GT { return GT() }
}
```

If both `A`

and `B`

are nonzero, they should have a `Pred`

typealias, which we can use, recursively:

This doesn’t work. I’m fairly sure this is a definitive dead end. Here’s the error: `ambiguous reference to member 'r'`

. The problem is that that error encapsulates exactly what I’m trying to achieve: I *want* the reference to be ambiguous, so it *depends* on the types of `A`

and `B`

. Most other routes I went down hit similar roadblocks:

The idea here was that you could have various implementations of `r`

, so that the `Result`

typealias would be inferred. The problem is the compiler wants to figure out what `Result`

is when you make a type that conforms to the protocol, so every type will get the default implementation.

Yet more versions I tried all hit the `ambiguous`

error, which makes me think this kind of thing is fundamentally impossible in Swift’s current form.

So I’ve got to break one of the rules: no more arbitrary numbers.

```
struct AddOne<N : Nat> {
typealias Result = Succ<N>
}
struct AddTwo<N : Nat> {
typealias Result = Succ<AddOne<N>.Result>
}
```

And so on. Or:

```
extension Binary where A == B {
var sub: Zero { return Zero() }
var com: EQ { return EQ() }
}
extension Binary where A == Succ<B> {
var sub: One { return One() }
var com: GT { return GT() }
}
```

Which can give you subtraction.

## Let’s Pretend to be Useful

All of that stuff is interesting, but very *very* far from being useful.

The length-indexed list from the other day probably is useful, though. As well as being kind of cool and safe, there are some (minor) optimisations it can do.

The other dependent type staple is the heterogenous list.

Now, this isn’t just any heterogenous list: we’re not writing Python here. This is a *statically typed* heterogenous list. Swift has a construct very similar to this already: a tuple!

But tuples aren’t very extensible:

And you can’t work with them in terms that most lists can:

So that’s where another tuple type can come in. A la Rob Rix, we could make a right-recursive tuple, terminated by `()`

. There’ll be one overarching protocol:

```
protocol _AnyTuple : CustomStringConvertible {
var tDesc: String { get }
var count: Int { get }
typealias Arity : Nat
}
```

And the empty tuple:

```
struct EmptyTuple {}
extension EmptyTuple : _AnyTuple {
var description: String { return "()" }
var tDesc: String { return ")" }
var count: Int { return 0 }
typealias Arity = Zero
}
```

The descriptions are just there to give us a pretty printout. Here’s the tuple struct:

```
struct NonEmptyTuple<Element, Tail : _AnyTuple> { var (head, tail): (Element, Tail) }
extension NonEmptyTuple : _AnyTuple {
var count: Int { return tail.count + 1 }
var description: String {
return "(" + String(reflecting: head) + tail.tDesc
}
var tDesc: String {
return ", " + String(reflecting: head) + tail.tDesc
}
typealias Arity = Succ<Tail.Arity>
}
```

Now, to build a tuple. Since it’s right-recursive, it might look like this:

But there are two problems with that: first, the comma is not overloadable. That’s probably a good thing. Second, it doesn’t really look like a tuple.

Joe Groff solved the first problem (albeit by committing a mortal sin). Just use a unicode comma! The only one I could find that works has the delightful name of Hypodiastole.

Trying to find it in the character viewer each time was a pain, though. So I went with the boring vertical bar.

The second problem can be solved with some sneaky overloading. Here’s what these functions look like:

```
infix operator | { associativity right precedence 90 }
func |<E, T:_AnyTuple>(lhs: E, rhs: T) -> NonEmptyTuple<E, T> {
return NonEmptyTuple(head: lhs, tail: rhs)
}
func |<E, T>(lhs: E, rhs: T) -> NonEmptyTuple<E, NonEmptyTuple<T, EmptyTuple>> {
return NonEmptyTuple(head: lhs, tail: NonEmptyTuple(head: rhs, tail: EmptyTuple()))
}
```

We can now, finally, build a Tuple:

One little wrinkle with protocols, though. If you try this:

There’s an error: `neither type in same-type refers to a generic parameter or associated type`

. Generally speaking, `==`

requirements in struct extensions don’t work. However, they do work on protocols. So a wrapper protocol is needed:

```
protocol Tuple : _AnyTuple {
typealias Head
typealias Tail : _AnyTuple
typealias Arity : NonZero
var head : Head { get }
var tail : Tail { get }
}
extension NonEmptyTuple : Tuple {}
```

Alright. Time to work with it.

```
extension Tuple where
Head : IntegerArithmeticType,
Tail : Tuple,
Tail.Head : IntegerArithmeticType,
Arity == Two {
func matSum(with: Self) -> NonEmptyTuple<Head, NonEmptyTuple<Tail.Head, EmptyTuple>> {
let a = head + with.head
let b = tail.head + with.tail.head
return (a | b)
}
}
(1 | 4).matSum(3 | 2) // (4, 6)
```

The basic advantage of this heterogenous list in Swift is its extensibility: you can treat tuples of length 2 as a type, or tuples where the third element is comparable as a type, and so on.

```
extension Tuple where Tail : Tuple, Tail.Head : Comparable {
func isSecondLessThan
<T : Tuple where T.Tail : Tuple, T.Tail.Head == Tail.Head>
(with: T) -> Bool {
return tail.head < with.tail.head
}
}
let a = (1 | 3.0 | "a" | 43)
let b = ("c" | 4.0 | 1)
a.isSecondLessThan(b)
```

Most of this stuff is madness. The custom infix unicode operator should have tipped you off to that: but it’s not to say that *nothing* here is useful. Compile-time warnings are great. I think the fixed-length array works. But this tuple stuff is too hacky: it only becomes useful if there are some low-level changes to the language.

What’s really useful, though, is *thinking* about types with dependency in mind. Getting familiar with what is and isn’t possible to write between the `where`

and the `{`

in an extension gives you a good idea of how powerful protocols and their specialisations are.

For some extra reading, check out DependentHaskell, Heterogenous Collections in Haskell, and Strongly Typed Heterogenous Collections. I’m muddling my way through seeing what’s possible with length-indexed lists, heterogenous lists, and numeral types over here, if you’re interested.