In Further Praise of Dependent Types
I&#x27;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:<p>- The most popular motivation: the ability to write proofs about your programs, using the same language for both programming and proving. It&#x27;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.<p>- Of course, you can also use dependent types to just write proofs for the purpose of doing mathematics, without any programming. I&#x27;ve written about my experience doing that here: <a href="https:&#x2F;&#x2F;www.stephanboyer.com&#x2F;post&#x2F;134&#x2F;my-hobby-proof-engineering" rel="nofollow">https:&#x2F;&#x2F;www.stephanboyer.com&#x2F;post&#x2F;134&#x2F;my-hobby-proof-enginee...</a><p>- But dependent types are also useful in ordinary everyday programming! Many &quot;features&quot; 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&#x27;t need special support for generics—you get it for free!<p>- 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!<p>- Of course, there&#x27;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.<p>- Haskell&#x27;s generalized algebraic datatypes are another example of a limited special case of the full power you&#x27;d get from a dependently typed programming language.<p>- Another example: some languages have special support for existential types in some form or another. For example, Rust has  something called &quot;impl Trait&quot; which is a limited use of existential types. This is another thing you get for free with dependent types (or rank-2 polymorphism).<p>- Other examples of things you get for free with dependent types: type aliases, higher-kinded types, higher-rank types, and compile-time code execution.<p>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.