Dependent Types: I”m Missing Something

owensd

I’ve been seeing a bunch of mentions about dependent types on Twitter lately and saw this blog post get mentioned.

Clearly I’m missing something.

The goal is provably correct code. Ok, I’ll suspend the fact that in the real-world computer hardware actually fails or memory can be corrupted, and I’ll focus on the provability of the code being provably correct in the abstract sense.

I still don’t get it.

One of the article’s example is this:

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
}

Ok… let’s continue on.

Dependent types are provided to fix 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 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?

I need to go and author more proofs to validate that the dependent types are all indeed correct.

Joe Groff tweeted this for some potential clarification:

//platform.twitter.com/widgets.js
In that link, we can see this example:

Definition negb (b : bool) : bool :=
match b with
    | true => false
    | false => true
end.

Definition negb' (b : bool) : bool :=
if b then false else true.

Theorem negb_inverse : forall b : bool, negb (negb b) = b.
destruct b.

But here’s the problem, this code also satisfies the proofs given so far:

Definition negb (b : bool) : bool :=
match b with
    | true => true
    | false => true
end.

Definition negb' (b : bool) : bool :=
if b then true else true.

Theorem negb_inverse : forall b : bool, negb (negb b) = b.
destruct b.

It’s up to the programmer to realize that we have actually not created all of the proofs required to prove correctness. So here’s my fundamental question: how do we know that we have enough proofs to actually prove our code is correct? I’ve only briefly looked over the topic, so maybe I’m simply missing the answer to this.

The paper does provide that last proof that we need:

Theorem negb_ineq : forall b : bool, negb b <> b.
destruct b; discriminate.
Qed.

But again, my question is how can we prove that we indeed have all of the proofs we need? Without that proof, I simply do not understand how dependent-types can actually produce provably correct code.

It’s an interesting topic; I’m not arguing against that or it’s application in domain spaces. I’m just trying to grok how this is objectively better than non-dependent-typed code with good test coverage. From a complexity standpoint, to me, it looks like a big loss; I get others will have less trouble on that end.

Dependent Types: I”m Missing Something