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

- Pierce, Types and Programming Languages (TaPL), or
- Harper, Practical Foundations for Programming Languages (PFPL).

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.