Thinking in types

Types can cause a lot of pain. They tend to inflexibly demand a way of programming which isn’t always effective and can seriously slow down your work. There’s also a big ergonomics problem. Type systems are notorious for verbosity and truly awful error messages.

Yet, people who are familiar with them don’t often have the same feeling. On one hand, familiarity helps soften a lot of that pain. The bad error messages don’t seem so bad once you’re used to them. But there’s something else, too.

Types influence the way you think about programs, and that influence is actually what makes them valuable.

The way to become comfortable with types is to embrace that influence. It can change how you think about and communicate about programs you read and write. Types aren’t a silver bullet—there are problems today where it’s not clear whether they help—but they’re a really good tool to own.

Continue reading “Thinking in types”

The shapes of data

It can be a bit of a pain to think about the various “shapes of data” available across languages. Often in learning a new language you might seek a “Rosetta Stone”. It’s valuable to be able to translate common shapes from one syntax to another. At the same time, it’s not always possible to make all of these translations cleanly. It can seem like some shapes are available in some places and not others.

Let me share my Rosetta Stone. It’s more fundamental, and thus widely applicable, than others. It’s also likely to be familiar to you because it’s exactly the same things you learned in high school algebra.

Continue reading “The shapes of data”

My favorite type theory book

I often see questions about what to read to learn type theory and I recommend Harper’s Practical Foundations for Programming Languages (PFPL). To be clear, this book is not a good recommendation if you want to learn more practically how to think in types. It’s instead a deep dive into what are types, why do they work, and how do we design practical type systems which cover the features we see in many programming languages.

Continue reading “My favorite type theory book”

Classes and types are different

Some language designs, most notably Java, conflate classes and types. They even go further by conflating subclassing and subtyping. This might be convenient but it causes a lot of pain.

Without a clear line for how they’re distinct it becomes hard to understand how either one really works. It makes certain language features and design tradeoffs opaque. For instance, it is key for understanding “type erasure”. It lies at the basis for why Scala’s TypeTags are different from Java’s ClassTags. It can also be an underlying thing that makes variance more difficult to understand.

Finally, certain design advice like the Liskov Substitution Principle actually apply to types and not classes. When using a language which conflates these ideas you still have to design your classes to respect LSP, but there’s a subtle sleight of hand occurring.

Continue reading “Classes and types are different”

Learning to love the type checker

The type checker isn’t your enemy at first. When you write hello world in your new typed language and you try to pull a fast one. You pass a number in where it’s expecting a string and just double check the checker. Is it really paying attention? Then a little later you legitimately make a silly mistake and it catches you still—good one you!

No, you hate the type checker when you’re trying to get work done and it just won’t damn shut up already! This is perfectly good code! Or maybe you’ve made a little typo. Do you really need 8 pages of compiler errors telling you how a module you haven’t touched in 4 days isn’t happy either? Really?

In most languages (a few lovely ones excepted) the errors are just awful, too. Sure, you can pick through them. Maybe 50% of the time figure out what they’re really whining about, but it’s a mess.

Is this really anything anyone recommends? Is something so miserable really worth the high praise?

Well, no. There’s a different way that experts use type systems.

Continue reading “Learning to love the type checker”

What even is a type?

You don’t really need to know what a type is in order to make great use of them. That said, not knowing what they are can be disconcerting. If you want to be able to communicate fluently with the type system then you should understand the major noun. More to the point, knowing what they are can help you to think in types.

It can be a little confusing to understand what a type is, though. It’s easy to at first say that they’re “sets of objects or values”, but that doesn’t necessarily part the fog of mystery. Fortunately, there’s a good way to understand types using one simple diagram.

Continue reading “What even is a type?”