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:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
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
1 2 3 4
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
vs working with terms in those types (like
"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
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:
1 2 3
This would be just as correct as far as the compiler is concerned as either of these definitions:
1 2 3 4 5 6 7 8 9 10
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
LEQ type that must provide evidence for how
particular are related:
1 2 3 4 5 6 7 8 9 10
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:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
This burden of proof would rule out both of our bogus definitions of
- In the flipped case, we would find we couldn’t prove an untruth.
- In the constant case, we couldn’t generate any proof by flat-out ignoring our inputs. We have to examine them and work with them to arrive at a proof of their relationship, and the type ensures it is indeed the relationship between those specific values.
We can now write a type-correct version with these new types, one whose return type captures the relationship between the two input terms:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
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
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.
- Totality, and why you should care
- How you can do real work without general recursion, or, how
Turing completeness has caused you generally avoidable pain
- I’d write about these now, but they’ll come up in more detail when I write up my notes on Turner’s “Total Functional Programming”.
- Interactive type-directed editing, where you cooperate with the compiler to
write your program, since very specific types lead to very specific shapes of
programs working with those types
- Faking up a DTSwift example of this would be a blog post in itself.
- Approximations to dependent types that have shown up already in some
not quite (not yet?) dependently-typed languages
- Spoiler: Swift isn’t one of them.
…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).