Why Dependent Types Matter

Jeremy W. Sherman:

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.

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.

[…]

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.

[…]

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.

Update (2015-09-04): Joe Groff recommends Certified Programming with Dependent Types.

David Owens II:

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 depedently-typed code? Why? What’s preventing me from swapping left and right in the Order type that is returned?

Update (2015-10-04): Jeremy W. Sherman:

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.

Jeremy W. Sherman:

David’s concern is that, “It’s up to the programmer to realize that we have actually not created all of the proofs required to prove correctness.” This concern arises from his thinking that the proof for negb_inverse goes through even if you alter negb so it always returns true.

The version of negb he defines that always returns true actually already fails at the negb_inverse theorem, without need to proceed to trying to prove negb_ineq.

[…]

David’s core concern about knowing you’ve proved what you want to prove is a real problem.

CS Theory Language Design Programming Swift Programming Language

2 Comments RSS · Twitter

Leave a Comment

Name

E-mail (will not be published)

Web site

Δ