## 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
f(i: Int) -> AnyObject {
func 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)
}
f(i: Int) -> SumType {
func 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:

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

Once you encode some numbers by hand:

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

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

```
<One, Two>.Result // Three
Sum<Five, Nine>.Result // LT
Comp<Four, Four>.Result // EQ Comp
```

## 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:

```
= [1, 2, 3, 4, 5].reverse()
let ar = AnySequence([1, 2, 3, 4, 5]).reverse() let se
```

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:

```
{
protocol BinaryOp : Nat
typealias A: Nat
typealias B}
```

Then, we can extend it, like this:

```
{}
struct EQ == B {
extension BinaryOp where A Result = EQ
typealias }
```

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`

:

```
<E0: Nat, E1: Nat> : BinaryOp {
struct Comp= E0
typealias A = E1
typealias B }
```

Only instances where `A`

and
`B`

are equal will get the type
alias:

```
<One, One>.Result
Comp<One, Two>.Result // Error Comp
```

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

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

```
{}
struct NEQ {
extension BinaryOp Result = NEQ
typealias }
```

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() }
}
== B {
extension BinaryOp where A 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.

```
<One, One>().r // EQ
Comp<One, Two>().r // NEQ Comp
```

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:

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

Then, any non-zero is bigger than zero:

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

If both `A`

and `B`

are nonzero, they should have a `Pred`

typealias, which we can use,
recursively:

```
: NonZero, B : NonZero {
extension BinaryOp where A var r: ?? {
return Comp<A.Pred, B.Pred>().r
}
}
```

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:

```
{
protocol BinaryOp : Nat
typealias A: Nat
typealias BResult
typealias var r: Result { get }
}
```

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.

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

And so on. Or:

```
== B {
extension Binary where A var sub: Zero { return Zero() }
var com: EQ { return EQ() }
}
== Succ<B> {
extension Binary where A 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:

```
: Comparable {...
extension Tuple where First == Two {... extension Tuple where Count
```

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

`(1, "a", 2.0) + ("b", -3)`

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:

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

And the empty tuple:

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

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

```
<Element, Tail : _AnyTuple> { var (head, tail): (Element, Tail) }
struct NonEmptyTuple
: _AnyTuple {
extension NonEmptyTuple 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
}
= Succ<Tail.Arity>
typealias Arity }
```

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

`1 , "a" , 4.0 , ()`

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.

`{ associativity right precedence 90 } infix operator ⸒ `

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:

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

We can now, finally, build a Tuple:

`(1 | 2.0 | "a" ) // (1, 2.0, "a")`

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

`== Two {... extension NonEmptyTuple where Arity `

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:

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

Alright. Time to work with it.

```
extension Tuple where: IntegerArithmeticType,
Head : Tuple,
Tail .Head : IntegerArithmeticType,
Tail== Two {
Arity matSum(with: Self) -> NonEmptyTuple<Head, NonEmptyTuple<Tail.Head, EmptyTuple>> {
func = head + with.head
let a = tail.head + with.tail.head
let b 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.

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

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.