Read: Why dependent types matter

By: Jeremy W. Sherman. Published: . Categories: reading-notes dependent-types.

Altenkirch, Thorsten, Conor McBride, and James McKinna. Why Dependent Types Matter. 2005. 19 pages (+2 more of references). Accessed 2015-08-26.

What is a dependent type?

A dependent type is a type that depends, not just on other types, but on terms. This means you can have values – plain old data – in your types. A common example is that of length-indexed lists:

/// A list parameterized by `ElementType` and indexed over its length.
/// This means that `Vector(length: 3, ElementType: Int)` is a different
/// *type* than Vector(length: 4, ElementType: Int)`.
///
/// You can read a type `Vector(n, T)` as "the type of vectors containing
/// precisely *n* Ts".
enum Vector(length: UInt, ElementType: Type) -> Type {
    /// Returns an empty list of inferred type `type`.
    case vnil():
        Vector(length: 0, ElementType: type)

    /// Prefixes an `element` whose type matches `vector`'s ElementType.
    ///
    /// NOTE: The type of the result vector differs from the type of the input
    /// vector by being one greater than the input.
    case vcons(element, vector: Vector(length: n, ElementType: type))
      where element is type:
        Vector(length: n + 1, ElementType: type)
}

You likely caught on that that code is Swift-ish but not actually Swift. That’s DTSwift*, where I pretend that Swift is dependently typed.

Types are terms are types

Notice that I’m writing the type constructor using normal function application with parentheses () rather than “generic type application” with angle brackets <>:

enum Vector(length: UInt, ElementType: Type) -> Type {
// NOT: enum Vector<length, ElementType> {
// The <> assume that everything in them is a type, which just ain't so
// in DTSwift.

As far as DTSwift is concerned, a type constructor is just a function from some terms/types to a type. We no longer need separate, parallel languages for working with types (like Int or String) vs working with terms in those types (like 3 or "perish the thought").

Why do we care?

Provably correct code where you want it, loosey-goosey where you don’t

Dependent types make it possible to be very specific about the terms in a type. We don’t have to be, but now we have the option of cranking up the specificity from “eh, whatever, gimme a list” to “this list has to be non-empty” to “this list has to have a prime number of elements”.

This means that dependent types give us pay-as-you-go provable correctness. You can require proof of the most critical properties in your program in the form of very specific types that ensure those invariants, while handwaving about components that are either less important or just more readily shown correct by test or inspection.

We can treat different data in different ways at compile-time

No need to wait to crash at runtime or during a test; you can push “make invalid states unrepresentable” to the max if you want.

Where Swift’s types let you down

Have you ever noticed how, if you write let order = x <= y ? .OrderedAscending : .OrderedDescending, you could swap x and y and still end up with a valid program? It’s like we learned nothing from that test we performed!

As far as normal Swift’s type system is concerned, any T is as good as any other; there’s “no means to express the way that different data mean different things, and should be treated accordingly in different ways” (p. 11). We can always just swap around the result of an if/else expression ?:, and our compiler will happily accept our backwards logic.

While we can write:

func compare(x: UInt, y: UInt) -> NSComparisonResult {
    return (x <= y) ? .OrderedAscending : .OrderedDescending
}

This would be just as correct as far as the compiler is concerned as either of these definitions:

func compare(x: UInt, y: UInt) -> NSComparisonResult {
    // BACKWARDS! IT LIES!
    // (And how many times have you accidentally flipped these?)
    return (x <= y) ? .OrderedDescending : .OrderedAscending
}

func compare(x: UInt, y: UInt) -> UInt {
    // I hope you weren't actually planning on relying on this function.
    return .OrderedAscending
}
Aside: Yes, this is a toy example

This is a toy example. I’m sure you can quickly figure out when an if-then-else has the branches swapped. Refining your code to use more specific types grows more valuable as the complexity of its behavior grows, and this is not a terribly complex example!

The effort/reward calculus changes when it comes to library code, though. Specific types in library code can save a lot of collective confusion and wasted time. Think of some Apple API you’ve looked at and gone, “Gee, I wonder what this method does when it runs into this corner case?” If the types clearly said what the method did, you wouldn’t be left scratching your head.

As a side benefit, specific types constrain your code to where the compiler can provide non-trivial help in writing the code. There’s a section on this in the paper, or just give a dependently-typed language a spin.

If you need to see some less toy examples to be convinced, check out Oury and Swierstra’s The Power of Pi (2008) and Fowler and Brady’s Dependent Types for Safe and Secure Web Programming (2013).

How dependent types fix this

Dependent types let you replace a Boolean that throws away the knowledge gained from a test by a type that represents the outcome of that test.

In DTSwift, we have the option of shifting from operator <=(left: UInt, _ right: UInt) -> Bool to a LEQ type that must provide evidence for how left and right in particular are related:

/// A type expressing that `(x <= y)` via proof by induction.
enum LEQ(x: UInt, y: UInt): Type {
    /// Base case: 0 <= any other UInt.
    case zeroLEQEverything:
        LEQ(0, y)

    /// Induction: If we know x <= y, then we also know x+1 <= y+1.
    case stepLEQ(LEQ(x, y)):
        LEQ(x + 1, y + 1)
}

We can then move from a “blind” NSComparisonResult to an Order type that expresses how two values are related and includes proof that this is indeed the case:

/// A type expressing the relationship between `left` and `right`.
/// Each case is associated with a term witnessing to the relationship
/// between `left` and `right`.
///
/// See: `LEQ(left, right)` defined just after this.
enum Order(left: UInt, right: UInt) -> Type {
    /// Represents that `(left <= right)`.
    /// Witnessed by a proof that `left <= right`.
    case lessThanOrEqual(because: LEQ(x: left, y: right)):
        Order(left, right)

    /// Represents that `(left >= right)`.
    /// Witnessed by a proof that `right <= left`.
    case greaterThanOrEqual(because: LEQ(x: right, y: left)):
        Order(left, right)
}

This burden of proof would rule out both of our bogus definitions of compare above:

We can now write a type-correct version with these new types, one whose return type captures the relationship between the two input terms:

func compare(left: UInt, _ right: UInt) -> Order(left, right) {
    switch left {
    case 0:
        return lessThanOrEqual(because: zeroLEQEverything)

    case let xMinus1 = left - 1:
        switch right {
        case 0:
            return greaterThanOrEqual(because: zeroLEQEverything)
        case let yMinus1 = right - 1:

            switch compare(left: xMinus1, right: yMinus1) {
            case lessThanOrEqual(because: evidence):
                // We know now that (x - 1) <= (y - 1), so we can prove
                // by adding 1 to each side that x <= y.
                return lessThanOrEqual(because: stepLEQ(evidence))

            case greaterThanOrEqual(because: evidence):
                // Ditto, but the evidence will show that (y - 1) <= (x - 1)
                // so we can prove y <= x AKA x >= y.
                return greaterThanOrEqual(because: stepLEQ(evidence))

            }  // switch on recursive call
        }  // switch on right
    }  // switch on left
}

Summary of the Example

We started with a compare function that did the right thing, but it didn’t say so – it just said “I’ll give you back a UInt, one’s as good as another, right?” (paraphrasing p. 12).

Because our starting version of compare didn’t say what it did via its types, it could also maybe not do the right thing; you could test it, but for all you know, some perverse developer decided to return the wrong answer for exactly one combination of unsigned integers.

We ended up with a compare that had no choice but to do the right thing, because if it didn’t, it would no longer typecheck.

So Much More

I encourage you to read this paper. It’s a great introduction to programming with dependent types, and it covers a number of other topics while demonstrating the topic by refining the implementation of merge-sort throughout.

You’ll meet:

…what we have tried to demonstrate here is that the distinctions term/type, dynamic/static, explicit/inferred are no longer naturally aligned to each other in a type system which recognizes the relationships between values. We have decoupled these dichotomies and found a language which enables us to explore the continuum of pragmatism and precision and find new sweet spots within it. Of course this continuum also contains opportunities for remarkable ugliness and convolution – one can never legislate against bad design – but that is no reason to toss away its opportunities. Often, by bringing out the ideas which lie behind good designs, by expressing the things which matter, dependent types make data and programs fit better. (p. 21)

*Since I don’t have a formal spec or implementation for this DTSwift fantasy language, it risks confusing things more than using an actual dependently-typed language, but I’m willing to take that risk to make this topic more approachable for people coming from Swiftland (population: 1 Gulliver).