What if you get your dependent type backwards?

David Owens II read my notes on “Why Dependent Types Matter” and asked a good question:

This is the part I don’t get: we allow for incorrect code to be written in the non-dependent-typed case, but we assume that we can’t do the same with dependently-typed code? Why? What’s preventing me from swapping left and right in the Order type that is returned?

Review: Backwards Booleans

If we’re not using dependent types, it’s not hard to flip the sense of a test and end up with a result that means the opposite of what we intended due to a hiccup in mentally simulating our code.

The running example is something like is(left: UInt, lessThanOrEqualTo right: UInt) -> Bool.

A Bool is just a bit that can be manufactured any which way, so this simple test fails to provide evidence – by which I mean constructive proof – for its claim.

If you switch to compare(left: UInt, to right: UInt) -> NSComparisonResult, you get more than a bit of info back, but you still can mess up. (If anything, it’s easier, since you now have to get 2 tests right to discrimate between the 3 cases rather than the 1 needed to decide between true/false in the Bool version.)

How do dependent types prevent backwards Booleans?

Now let’s say we’re using the dependent type Order(left: UInt, right: UInt):

enum Order(left: UInt, right: UInt) -> Type {  /* #1 */
    case lessThanOrEqual(because: LEQ(x: left, y: right)):  /* #2 */
        Order(left, right)  /* #3 */

    case greaterThanOrEqual(because: LEQ(x: right, y: left)):  /* #4 */
        Order(left, right)  /* #5 */
}

We have 5 instances of using left/right together, labeled in comments at the end of each line.

What’s preventing me from swapping left and right in the Order type that is returned?

Well, let’s see! David mentions swapping the left/right in the Order type that’s returned, which corresponds to #3 and #5, so we’ll start there.

Dropping the Evidence

Let’s drop the evidence (the because bits) and swap left/right #3 and #5:

enum OrderNoEvidence(left: UInt, right: UInt) -> Type {  /* #1 */
    case lessThanOrEqual:  /* #2 - eliminated */
        OrderNoEvidence(right, left)  /* #3 - flipped */

    case greaterThanOrEqual:  /* #4 - eliminated */
        OrderNoEvidence(right, left)  /* #5 - flipped */
}

In this case, nothing would catch the inversion. left and right are both UInt, so there’s no harm done as far as the compiler is concerned.

There’s also no actual distinction in shape between the two cases; we can freely substitute one for the other anywhere in our code without the type system griping, just as with Bool or NSComparisonResult.

Unlike the non-dependent type, an instance of this type carries around information at the type level about the values whose comparison it represents, so you can recover at least which values were supposedly compared through pattern matching.*

But this doesn’t solve our flipped-Boolean problem.

Restoring the Evidence

Now let’s restore our evidence in its un-flipped form, while leaving the resulting type still flipped in #3 and #5:

enum OrderFlippedInstances(left: UInt, right: UInt) -> Type {  /* #1 */
    case lessThanOrEqual(because: LEQ(x: left, y: right)):  /* #2 */
        OrderFlippedInstances(right, left)  /* #3 - flipped */

    case greaterThanOrEqual(because: LEQ(x: right, y: left)):  /* #4 */
        OrderFlippedInstances(right, left)  /* #5 - flipped */
}

We’ve flipped #3 and #5 still, but the rest are back and not flipped.

Compared to the evidenceless version of the type, you can no longer gin up an instance of Order out of thin air. You once again have to provide an instance of LEQ:

enum LEQ(x: UInt, y: UInt): Type {
    case zeroLEQEverything:
        LEQ(0, y)

    case stepLEQ(LEQ(x, y)):
        LEQ(x + 1, y + 1)
}

Alas, even with LEQ completely correct, we can still define this version of Order. It will compile just fine.

This might confuse the user of this API, especially if the documentation says that Order(left, right) tells how left compares to right rather than how right compares to left.

Unlike in the evidence-less case, though, consumers of instances of this type can work out that it’s the wrong way around based on the because evidence: an instance like lessThanOrEqual(zeroLEQEverything: LEQ(0, 1)): OrderFlippedInstances(1, 0) hands the consumer a proof that LEQ(0, 1), and if they pattern-match that out and use it – as they likely would while producing evidence for the correctness of whatever they’re building atop this data – it’s merely frustrating that our documentation is backwards.

This “solves” the flipped Boolean problem, but no tool can solve the problem of misleading names. Misleading names provide bad input into our informal reasoning processes, and we’re likely to write bogus code as a result. If we’re programming with evidence, as dependent types let us do, we’ll catch this while interacting with the compiler; if we’re trusting the names, and ignoring the evidence, as dependent types also let us do (and non-dependent types force us to do), we likely won’t, absent testing.

Flipping All Pairs

If we flip all pairs, we get something identical to our original Order(left: UInt, right: UInt) type:

enum OrderMirrored(right: UInt, left: UInt) -> Type {  /* #1 */
    case lessThanOrEqual(because: LEQ(x: right, y: left)):  /* #2 */
        OrderMirrored(right, left)  /* #3 */

    case greaterThanOrEqual(because: LEQ(x: left, y: right)):  /* #4 */
        OrderMirrored(right, left)  /* #5 */
}

Aside from the backwards parameter names if you look at the definition or documentation, this works the same as the original Order. Even the case names are the right way around.

Providing the Wrong Evidence

If we accept the wrong evidence, by flipping around just #4, then we finally get real breakage:

enum OrderWrongEvidence(left: UInt, right: UInt) -> Type {  /* #1 */
    case lessThanOrEqual(because: LEQ(x: left, y: right)):  /* #2 */
        Order(left, right)  /* #3 */

    case greaterThanOrEqual(because: LEQ(x: left, y: right)):  /* #4 - flipped */
        Order(left, right)  /* #5 */
}

By flipping #4, we’ve ended up with two cases with different names that just say the same thing. This is clear because they have the same shape: each takes one argument of the same type, and each constructs an instance of the same type.

Again, if you’re leaning on that evidence, this will work itself out while you’re writing code, because you’ll reach for the expected y <= x proof when handling the greaterThanOrEqual case only to find it’s not there.

If the client code is more trusting and ignores the evidence, then you’ll get broken behavior, and you won’t find it till you test the code by running it.

Dependent types allow us to provide and demand evidence

This is the trade-off you’re able to make when using dependent types:

• trust and test,
• or demand proof.

Without dependent types, you don’t have any proof – you’re left to trusting and testing.

*Dependent pattern matching can bind values not just out of the instance, as normal pattern matching does with case let, but also out of the type signature.