What are types?

When people first hear about type theory, they often ask a very basic question: what are types actually?

A good starting point is this: the question Is this value of type X? asks whether a value belongs to some group, class, or family of values described by X. In other words, a type is at least a criterion of membership. If 3 : Int, then 3 belongs to the family of integer values. If "hello" : Str, then that string belongs to the family of string values.

This is not the whole story, but it is the right first question. A type is a way to divide values into those that members of a given set, and those that don't. Once we understand that, we can ask what extra structure a type carries beyond mere membership.

Values do not float in a vacuum

Before we talk about types, it helps to ask what a value is. In mathematics and logic, values are usually not primitive magical objects. They are encoded inside some axiomatic foundation.

For example, in set theory one can encode ordinary mathematical values entirely in terms of nested sets. The natural numbers can be represented like this:

0 = {}
1 = {0}
2 = {0, 1}
3 = {0, 1, 2}

Pairs, functions, lists, relations, and more can also be encoded as sets. From the perspective of the foundation, there is only set membership and set construction all the way down. What we informally call a number or a function is, in that setting, a structured arrangement of sets.

Lambda calculus gives a different picture. There, a function can be used to define essentially any value. Booleans may be encoded as:

true  = λt. λf. t
false = λt. λf. f

Natural numbers may be encoded as Church numerals:

0 = λf. λx. x
1 = λf. λx. f x
2 = λf. λx. f (f x)

Pairs, lists, and other data can be encoded similarly. So even if two foundations talk about the same mathematical value, they may realize it using very different primitive machinery. Set theory nests sets. Lambda calculus composes functions. Type theory introduces judgments about inhabitants of types.

Types are not just labels

It is tempting to imagine that every value has one intrinsic label glued onto it, and that the type system merely reads that label back. That picture is usually too simple.

A single value can often inhabit many types. The number 3 might be an Int, a Number, an Eq value, an Ordered value, or a member of a refinement such as Positive. Types are therefore often better understood as different ways of classifying and using the same value, not as unique identity tags.

This is one reason the membership question is so useful. Rather than asking What label is attached to this thing?, we ask Does this value belong to the family described by this type? That shifts our attention from hidden essence to explicit criteria.

Why types matter

If types were only about grouping values into buckets, they would still be useful, but type theory usually wants more. A type typically describes not just what values count as inhabitants, but also what may be done with those inhabitants.

Suppose we say that some input has type Number. That may mean that arithmetic operations are valid on it. It need not mean that every possible property of the underlying representation is exposed. In fact, a well-designed type often hides many details while exposing only the operations that matter.

This is why the informal slogan a type is a set of values is helpful but incomplete. Types are more like structured classifiers. They answer a membership question, but they also carry rules about construction, observation, equality, and computation.

Static and dynamic checks ask the same question

People often contrast static and dynamic typing as though they were asking fundamentally different things. Usually they are not. Both are trying to answer some version of the question Does this value belong to this family? The difference is mostly when and how the answer is obtained.

A statically typed language tries to answer many of those questions before the program runs. A dynamically typed language answers them while the program runs. A language with rich predicates may treat types as runtime checks. But the logical shape is similar: classify the value, and then justify certain operations based on that classification.

Computational type theory

Type theory becomes especially interesting when types themselves are allowed to involve computation. In computational type theory, the type is not merely a passive annotation. It may contain expressions that must be evaluated in order to understand what the type even is.

For example, if a type depends on a value such as a length, then asking whether something has that type may involve normal evaluation of terms. The type is no longer just a static name from a closed catalogue. It is part of the computational world.

This is one reason type theory feels different from the informal set picture. In the set picture, one often imagines a fixed universe of sets and then asks whether an element is in one of them. In computational type theory, the type itself may be a computed description, and membership may depend on evaluating programs.

Types as specifications

Another useful way to think about a type is as a specification. If a function has type

f : A -> B

then that says more than f is some thing with a tag on it. It says that when given an inhabitant of A, the function is expected to produce an inhabitant of B. A type can therefore be read as a contract on use and construction.

In richer systems this becomes even more expressive. A dependent type may say that the output depends on the input. A refinement type may say that only values satisfying some predicate count. A capability-oriented type may say which operations are available while hiding everything else.

Types and propositions

Many type theories go one step further and identify propositions with types. Under this view, asking whether a type has an inhabitant is analogous to asking whether a proposition has a proof. A value inhabiting the type is the proof.

This is often called the Curry-Howard correspondence. It is the observation that logical propositions and program types line up surprisingly well. A proof of an implication behaves like a function. A proof of a conjunction behaves like a pair carrying both components. A proof of a disjunction behaves like a tagged choice between alternatives.

For example, the logical statement A -> B corresponds to a function that takes an inhabitant of A and produces an inhabitant of B. The statement A and B corresponds to a value containing both an A and a B. The statement A or B corresponds to a value that is either a left-tagged A or a right-tagged B.

This can sound strange at first, but it fits the membership perspective rather well. If a proposition is understood as the collection of its proofs, then the question Is there a value of this type? becomes Is there a proof of this proposition? The border between logic and programming becomes much thinner. In that sense, evaluation of programs and simplification of proofs are closely related activities.

A better intuition

So what are types, really?

They are not merely machine-level tags, and they are not always identical to naive mathematical sets. A type is best understood as a way of carving up the space of values together with a discipline for how those values may be introduced, transformed, and observed.

The simplest question remains the most illuminating one: when we ask whether a value is of type X, we are asking whether it belongs to the family of values described by X. Different foundations answer that question with different primitive machinery. Set theory encodes values as sets. Lambda calculus encodes them as functions. Type theory adds judgments about inhabitation, computation, and use.

From there, the rest of type theory grows naturally. Once we know how values are classified, we can talk about functions between classes of values, proofs as inhabitants, dependent types, interfaces, abstractions, and programs whose types themselves compute.

That is why type theory is worth studying. It is not merely about catching bugs. It is about making precise what kinds of values we have, what counts as using them correctly, and what sort of world our programs are actually built in.