What is a type system for?

I watched Alexis King's Constructive Data Modeling talk and was surprised by how simply the Parse, don't validate author and former Haskell compiler contributor defines what a type system is for, which features are necessary, and how precisely you should model your data:

The answer that I give is really much simpler than this, which is just that the type system keeps track of the different cases that you have to handle in your code. [...] A type system is really this sort of obligation propagation machine where each type definition relates the places where you produce values and the places you consume values, and it is those use sites specifically that inform what the obligations ought to be.

I probably would have said something about correctness and expressing your domain concepts clearly. Keeping track of cases to handle is a much simpler goal.

She argues three features are all you need to capture most invariants:

The main ingredients for the techniques that I'm going to be talking about require some form of product types, that is, types where you can just combine things together. So, tuples, structs, records, any of those. Some form of sum types, so things where you have different variants. So, algebraic data types, Rust calls those enums, TypeScript unions, sealed interfaces in Scala. And you need some ability to do exhaustive case analysis, pattern matching on those different variants of these types such that the compiler will tell you when there are some that are not covered. And that's it. [...] If you have a language that supports all these things, then all it takes to reap all these benefits is a shift in perspective.

Structs + enums + match statements. Or, records + unions + switch statements (etc, depending on your language). That's a short list! I would have expected someone who's spent most of her professional life writing Haskell (now Scala) and currently builds software people depend on for their medications to approach correctness with a bigger toolbox.

Most surprising to me was her recommendation to prefer simple primitive types by default and only add precision when that eliminates a runtime error:

There is no need to strengthen the types. There's no need to make them any more precise than they need to be, except when you have these situations where otherwise there could be an error raised at runtime. [...] I see a lot of people who have read “Parse, don't validate” and they get very confused because they think, well, I need to have some email address type that then pins down the type of every email address everywhere in my system. [...] I just represent email addresses as strings because there is not actually any situation where I would need to look at the structure of an email address.

On the one hand, that matches the general programming wisdom to avoid over-engineering and prefer the simplest solution that solves the problem. Optional complexity has a cost. In this case, precise types are a form of complexity to be avoided where possible.

On the other hand, using types to model domain concepts makes a system's intent clearer. A UserId and an InvoiceId are both strings, but they are not the same type of thing at all. Domain-specific types, newtypes, the typestate pattern etc may not always directly change runtime outcomes, but they tell a clearer story than primitive types and can make a system easier to understand and maintain over time.

But Alexis is very smart, so I'm going to keep thinking about this. 🤔