# What if you get your dependent type backwards?

*By:*.

*Published: .*

*Categories: dependent-types blogosphere.*

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.