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.

The heart of a type is how it classifies values

Types are classifications of values where values are what eventually result when we evaluate a valid program expression.

This is the simplest mode of thinking about types where you might even say something like the type of Boolean “contains” the values true and false and the type UnsignedInt32 contains all of the, well, unsigned 32-bit integers.

Thinking of types as sets which contain values is a good metaphor. It’s slightly better, though, to think of types as classifying values: given a particular value, you can tell me its type. With that, we can expand the drawing a little further.

The cornerstone of the meaning of types comes from their relation to values. They say some important facts about values but not everything. They are an approximation.

Types are most valuable, pragmatically speaking, for having a direct relation to programs, not the indirect one I’ve sketched above. In particular, a type system is valuable because I can give you the type of a program expression without evaluating it.

This is why types are best when they’re approximations. If I want to know the complete information about a program then I might need to evaluate. If I only need partial information, then I may be able to obtain it through inference.

Here inference essentially means “systematic guessing”. It’s the part of the type system where programs are analyzed—but, again, not evaluated—and a type returned. This type is only useful if it’s correct, of course. This is the final element of a type system: a guarantee.

If a type is shown to match an expression, then that expression evaluates to a value that would be classified at that same type.

Or, in diagram form, we add a big fat equals mark.

Okay, but then what really is a type?

The above discussion gets right at the heart of what a type means. A type is given meaning by how it relates to programs, values, and the evaluation relationship between them. But it also avoids the headliner question: what even is a type?

But the funny thing is that you probably already knew the answer to that question. A type is one of the things Integer, Float, or String. Or it might build from there when you talk about types like List[Integer] or function types like String -> Integer.

What I mean to say is that types are expressions in a language all their own, the type-language corresponding to the value-language of your programming language (what a mouthful!). In particular, this type-language is one that’s explicitly designed to be able to say interesting, approximate things about the corresponding value-language.

So, really, it’s hard to say anything terribly informative about what a type is without talking about those relations discussed above.

Further reading

There’s a great deal more to say about this topic. In fact, if you really read carefully what I wrote above then you’ll notice a lot of holes and inconsistencies.

You can get a lot deeper into this subject by listening to Ron Garcia’s excellent PWLConf 2017 talk. He additionally links a few references to academic papers where types (as they relate to programming languages) were first invented. I’ll also recommend Milner, A Theory of Type Polymorphism in Programming (1978) as being reasonably readable and interesting in its historic context.

The real way to dig in deep and get a picture here is to read one of the two canonical textbooks on type theory in programming languages, either

Though, if you choose to read Harper’s book then the standard advice is to skip to Chapter 4 and come back to the beginning later. There’s also a second edition preprint available of PFPL available from Harper’s website if you’d prefer to try before you buy.

2 thoughts on “What even is a type?

Comments are closed.