Type systems should be consistent (and probably dependently typed)

I personally believe that the most important property of a type system is that it has a really simple, consistent¹ core. If you don’t have this, you will accrue accidental complexity over time.

You can see this pretty well in Rust and TypeScript where, as an outsider, a lot of type system discussions are a bit strange to follow because it seems like they’re designing themselves into a corner much more than they’re arguing about anything fundamental to the problem they’re trying to solve. This isn’t a dig at either language, they both have pretty strong constraints that make them rely on very specific features so this is more or less inevitable. But they’re also both not exactly known for being simple, are they?

This is actually one of the main reason why I love full spectrum dependent types! Some people think dependent types are complex or difficult but that’s just because the ways to approximate them in languages like Haskell or OCaml are quite complex.

Dependent types on their own are actually much simpler than either of those languages! For example, OCaml’s module language sits on top of the regular term language and reinvents a lot of the term level concepts (functors, first class modules, (mutually) recursive modules, etc) with a lot of subtle but significant limitations. Similarly, Haskell’s type language reinvents a lot of what already exists in the term language (open/closed type families, type-level pattern matching, data kinds, etc.) with — you guessed it — a lot of subtle but significant limitations.

Dependent types make things much simpler because they collapse all of those languages — terms, types, kinds and modules — into a single one that behaves consistently.

With full spectrum dependent types, “can I do this with a functor/type family” isn’t even a question you need to ask because functors and type families are just functions and you should hopefully know what you can do with functions. If modules are just record-like values that happen to be usually known at compile time, then first-class-modules are just… modules that aren’t known at compile time. This isn’t even something you would think of as a feature, it’s just what naturally falls out of your type system if you remove all the arbitrary restrictions that a separate module language creates!

Even polymorphism itself goes from something relatively opaque (at least to beginners) about how a function “can work for every possible instantiation of a” to a dependent function with an implicit parameter that happens to have type Type. This even largely gives you higher-rank polymorphism for free because a higher-rank function is just a higher order function where the argument happens to take an argument of type Type.

If you want the simplest possible type system, it should probably have dependent types.