5 ms·
I've been meaning to write a tutorial on dependent types, but aimed at programmers rather than mathematicians and computer scientists. Here are some of the reas
by curryhoward 6y ago
I've been meaning to write a tutorial on dependent types, but aimed at programmers rather than mathematicians and computer scientists. Here are some of the reasons I love them so much:
- The most popular motivation: the ability to write proofs about your programs, using the same language for both programming and proving. It's so satisfying to write code and prove it correct (with a type checker to catch your mistakes), but so few people get to experience this feeling.
- Of course, you can also use dependent types to just write proofs for the purpose of doing mathematics, without any programming. I've written about my experience doing that here: https://www.stephanboyer.com/post/134/my-hobby-proof-engineering https://www.stephanboyer.com/post/134/my-hobby-proof-enginee...
- But dependent types are also useful in ordinary everyday programming! Many "features" of programming languages that we use at work are actually just limited special cases of the general idea of dependent types. For example, in a dependently typed language, you don't need special support for generics—you get it for free!
- Dependent types also eliminate much of the need for macros. In Rust, for example, you might use a macro to generate a JSON parser for a given type. If you had dependent types, you could just write a function that takes your type as an argument and returns the parser!
- Of course, there's that famous example of length-indexed vectors. The idea is that you can keep track of the sizes of your arrays in their types, and statically prevent out-of-bounds errors. So, for example, trying to get the first element of an empty array would be a type error.
- Haskell's generalized algebraic datatypes are another example of a limited special case of the full power you'd get from a dependently typed programming language.
- Another example: some languages have special support for existential types in some form or another. For example, Rust has something called "impl Trait" which is a limited use of existential types. This is another thing you get for free with dependent types (or rank-2 polymorphism).
- Other examples of things you get for free with dependent types: type aliases, higher-kinded types, higher-rank types, and compile-time code execution.
Dependent types may seem complicated at first glance. But after seeing how all these programming language features collapse into a single unified framework, you might change your mind: dependent types are extremely simple compared to the cornucopia of concepts we have to learn in their absence! I strongly believe that programming languages have grown too complex, and dependent types have the right power-to-weight ratio to cull that complexity.
- haneefmubarak 6y agoI, for one, would be quite fascinated by such a blog post - you make it sound downright magical! I'm curious, are there languages that in your opinion support dependent typing well enough to allow all the concepts that you are describing? Also, does support of dependent types suggest, imply, or require a particular paradigm (function, imperative, procedural, declarative, etc) or is that an orthogonal concern?
- curryhoward 6y agoMaybe with shelter-in-place I'll have time to write it. :) > I'm curious, are there languages that in your opinion support dependent typing well enough to allow all the concepts that you are describing? Most of my experience with dependent types comes from a language called Coq (as well as one of my side projects, which is a new dependently typed language). Agda and Idris (among others) also support this style of programming. Idris goes further and uses dependent types to provide amazing IDE capabilities. There's a YouTube video where the designer of Idris used his IDE to automatically implement matrix transposition (the type was so precise that the compiler discovered the only sensible implementation). Unfortunately I think the world is still lacking a good general-purpose dependently typed programming language suitable for production use (though I'm working on it). > Also, does support of dependent types suggest, imply, or require a particular paradigm (function, imperative, procedural, declarative, etc) or is that an orthogonal concern? Generally speaking, dependently typed languages are functional. The fundamental concept in dependently typed languages is the dependent function type, also called "pi type" or (confusingly) "dependent product type". So, the whole thing is based on functions and their types. One could imagine some kind of hybrid language, but combining dependent types and implicit side effects (like imperative languages have) is an active area of research.
- vlaaad 6y agoDamn, this area of programming sounds very interesting, but I'm so so lost in these type compositions... Is it this Idris video you are talking about? https://youtu.be/X36ye-1x_HQ?t=1716 https://youtu.be/X36ye-1x_HQ?t=1716 I'm already having troubles following it after 8 lines of type definitions, while matrix transposition in the language of my choice is just `#(apply mapv vector %)` Sorry, I'm not trying to be dismissive, I just want the ergonomics of expressing my intentions to the computer be free of all this boilerplate while leaving compiler a possibility to give me some useful feedback when something might be wrong, are we really not there yet or are there languages aiming to make dependent types practical? You mentioned Coq, but I'm still not being able to find any code examples or some getting started guide in its official documentation...