In which I Misunderstand Dependent Types

All of this available as a shiny, fancy playground here.

So there was a blog post the other day about dependent types:

Why Dependent Types Matter

Most blog posts that deal with the more mathematical/category theory side of programming go over my head when I read them, only to become suddenly clear a few weeks down the line. I have not reached this such sudden clarity with this post, but I’m starting to see a glimmer.

In particular, I was reminded of this post on the Apple developer forums. It describes a way to write a generic vector type, with the length of the vector encoded into the type. Sounds a lot like length-indexed lists, no? I thought so.

Basically, the type was recursive. An empty vector has the type of `EmptyVector`, a vector of length 1 has the type of `Vector<EmptyVector>`, of length 2 is `Vector<Vector<EmptyVector>>`, and so on. Both the struct `Vector` and `EmptyVector` conformed to the protocol `VectorType`, which allowed for the polymorphism.

Inside the struct, the values were managed in a recursive-list style. Indexing looked kind of like this:

```public protocol VectorType {
typealias Element
var startIndex: Int { get }
var endIndex: Int { get }
subscript(i: Int) -> Element { get set }
}

extension VectorType {
var startIndex: Int { return 0 }
}

struct EmptyVector<T> : VectorType {
typealias Element = T
var endIndex: Int { return 0 }
subscript(i: Int) -> Element {
get { fatalError("Index out of range") }
set { fatalError("Index out of range") }
}
}

struct Vector<H, Tail: VectorType where Tail.Element == H> : VectorType, CollectionType {
typealias Element = H
var tail: Tail
subscript(i: Int) -> Element {
get { return i == 0 ? head : tail[i - 1] }
set { if i == 0 { head = newValue } else { tail[i - 1] = newValue } }
}
var endIndex: Int {
return tail.endIndex + 1
}
}

vec     // 1
vec     // 2
Array(vec) // [1, 2, 3]
```

And through the indexing, the vector could conform to `CollectionType`.

As you can see, though, it’s not very efficient for iteration, or subscripting. The normal recursive list would be iterated like this:

```enum List<Element> : GeneratorType, SequenceType {
case Nil
indirect case Cons(Element, List<Element>)
mutating func next() -> Element? {
guard case let .Cons(x, xs) = self else { return nil }
self = xs
return x
}
}
```

So on every `next()` call, `self` is replaced by the tail (`xs`), and the head (`x`) is returned. However, because a vector’s type is dependent on its length, you cannot replace `self` with its tail, because the tail is a different type. So for every index call, all the predecessors in the vector must be traversed.

In fact, what we’re looking for isn’t really a recursive list at all. It’s certainly elegant, and it has all that cool functional allure, but it’s not necessary. All we really care about is the length: we want to encode that as a type. So let’s do it! Here again, protocols are going to give us the required power.

So, what kind of thing is length? Well, it will be an integer greater than or equal to zero. A natural number, then:

```public protocol Nat {}
```

We don’t want it to carry any values, because all we’re interested in should be resolved at compile-time. We’re going to have to use types inference like control flow for a bit, in order to get what we want. The first number to encode is 0:

```public struct Zero : Nat {}
```

And then one, two, and so on. Except that’s silly. Obviously what we want is some more of that recursion. So a new protocol, then:

```public protocol NonZero : Nat { typealias Pred : Nat }
```

So it has a typealias `Pred`: representing the number that comes before it. `Pred ` can be any natural number. Let’s make a struct conform:

```public struct Succ<P: Nat> : NonZero { public typealias Pred = P }
```

This works just as you’d expect: `Succ` is the successor to `N`. So, for instance, one two and three look like this:

```typealias One   = Succ<Zero>
typealias Two   = Succ<Succ<Zero>>
typealias Three = Succ<Succ<Succ<Zero>>>
```

Now, we can use these as generic types to go along with any structs we want. They don’t carry any values, so there’s no overhead. Let’s make a constant-sized array:

```public struct ConstArray<Element, Count : Nat> {
private var contents: [Element]
}
```

It’s no good without an initialiser. Now, exposing one would be pretty useless: you could just create a `ConstArray<Int, Succ>()`: an array with a different length to the one its type states. A free function is the other option:

```public func emptyArray<E>() -> ConstArray<E, Zero> { return ConstArray(contents: []) }
```

To build arrays, a function can take a given array, and then return an array with the corresponding extra length:

```public extension ConstArray {
func appended(with: Element) -> ConstArray<Element, Succ<Count>> {
return ConstArray<Element, Succ<Count>>(contents: contents + [with])
}
func prepended(with: Element) -> ConstArray<Element, Succ<Count>> {
return ConstArray<Element, Succ<Count>>(contents: [with] + contents)
}
}
```

You’ll notice none of these functions are mutating: you can’t change the length without affecting the type, and we can’t change the type in Swift at all. So the usual `append` becomes `appended`, and so on.

Since arrays will have to be built this way, a custom operator is probably justified:

```infix operator +| { associativity left precedence 90 }

public func +| <E, N : Nat>(lhs: ConstArray<E, N>, rhs: E) -> ConstArray<E, Succ<N>> {
return lhs.appended(rhs)
}

infix operator |+ { associativity right precedence 90 }

public func |+ <E, N : Nat>(lhs: E, rhs: ConstArray<E, N>) -> ConstArray<E, Succ<N>> {
return rhs.prepended(lhs)
}
```

Add a `description`, and the new arrays look like this:

```extension ConstArray : CustomStringConvertible {
public var description: String {
return contents.description
}
}

emptyArray() +| 1 +| 2 +| 3 // [1, 2, 3]
```

Now, iteration will be as efficient as native array iteration. Making the struct `MutableSlicable` should be easy, also:

```extension ConstArray : MutableSliceable {
public var startIndex: Int { return contents.startIndex }
public var endIndex: Int { return contents.endIndex }
public subscript(i: Int) -> Element {
get { return contents[i] }
set { contents[i] = newValue }
}
public subscript(i: Range<Int>) -> ArraySlice<Element> {
get { return contents[i] }
set { contents[i] = newValue }
}
}
```

This is where things get cool. How about a function that only takes arrays of the same length?

```func onlySameLength<A, B, C : Nat>(lhs: ConstArray<A, C>, rhs: ConstArray<B, C>) {}

let twoLong = emptyArray() +| 1 +| 2
let twoChar = emptyArray() +| "a" +| "b"

onlySameLength(twoLong, rhs: twoChar)

let threeInts = emptyArray() +| 1 +| 2 +| 3

onlySameLength(twoLong, rhs: threeInts) // error
```

How about functions that remove items from an array? They won’t be able to mutate anything, they’ll have to return the item and the shorter array in a tuple, but that’s par for the course in some languages. Let’s try it:

```public extension ConstArray {
func removeLast() -> (Element, ConstArray<Element, /** What to put here? */ Zero>) { fatalError() }
}
```

So what are the types it should return? The count of the `ConstArray` should be one less than the count of self, obviously. Not all types that conform to `Nat` have a `Pred` typealias, though. Only the nonzeroes. Luckily, we have a protocol for that: `NonZero`. So here’s what our extension signature looks like:

```public extension ConstArray where Count : NonZero {}
```

That is awesome. Just by the logic of the types themselves, we’ve found that we can only define remove operations on arrays with nonzero lengths! Here’s what they look like:

```public extension ConstArray where Count : NonZero {
func removeLast() -> (Element, ConstArray<Element, Count.Pred>) {
var temp = contents
return (temp.removeLast(), ConstArray<Element, Count.Pred>(contents: temp))
}
func removeFirst() -> (Element, ConstArray<Element, Count.Pred>) {
var temp = contents
return (temp.removeFirst(), ConstArray<Element, Count.Pred>(contents: temp))
}
func removeAtIndex(i: Int) -> (Element, ConstArray<Element, Count.Pred>) {
var temp = contents
return (temp.removeAtIndex(i), ConstArray<Element, Count.Pred>(contents: temp))
}
}
```

So there you go! dependent types can (kind of) happen in Swift.

1. · September 5, 2015

Your vector recursive things doesn’t perform like simd and it is recursive … :((
Why somebody would want this when Swift 2 supports simd.

Like

• · September 7, 2015

Well, first off, I don’t want to take credit for the vector implementation. What you see here is an adaption of Dave Abraham’s implementation, which is linked above.

Secondly, it’s really not intended to replace SIMD, or anything like it. It’s more of a proof-of-concept of one of the textbook patterns for dependent types. The vector in particular is a toy example. The ConstArray, though, is possibly useful.

Like

2. Pingback: Yet More Misunderstanding of Dependent Types | Big O Note-Taking
3. Pingback: Emptiness 空值语义-IT文库
4. Pingback: Emptiness 空值語義 | 程式前沿
5. Pingback: Emptiness 空值語義 - 程序員的後花園