Type theory

Type theory is a branch of mathematical logic and computer science that focuses on how we classify and understand information, especially as it relates to programming and mathematics. Generally, it helps us answer the question:

What kind of data is this?

When you write TypeScript programs, you are using a software compiler that provides a formal framework to describe and reason about these "kinds of data" (types), the values they contain, and the rules governing their interaction.

Everything has a type

A core principle of type theory is that everything has a type. In this guide, we will use mathematical notation like for numbers and for strings.

The key difference between using string in TypeScript and in type theory is that the former is a programming construct, while the latter is part of a more rigorous definition about it means to be a string. Mathematical types are more than labels - they define the rules for how terms behave and how they can be composed.

Notation

Consider this simple function which adds two numbers.

We would formally say the function add has the type .

Currying

One important idea in type theory is currying, named after the logician Haskell Curry. Currying is a process by which a function that takes multiple arguments is transformed into a sequence of functions that each take a single argument.

Consider the curried form of the add function above.

This transformation is fundamental to how we think about functions in type theory.

Types as propositions

One of the most profound insights in type theory is the Curry - Howard correspondence, which posits that

Types are Propositions and Programs are their Proofs.

That is, if you have a value of type , you can think of this as a "proof of the proposition ". Similarly, a type like corresponds to the logical implication "if is true, then is true".

The product type corresponds to conjunction - "A and B are both true".

The sum type corresponds to disjunction - "either A or B is true".

Dependent function types

A Π-type (pronounced "pi-type") is a dependent function type, which generalizes a regular function type like to allow the output type to depend on the input value. Formally, it may be written as

This means "for every of type , the type of the result is ". Essentially, the type of the result may depend on the value of .

Dependent pair types

A Σ-type (pronounced "sigma type") is a dependent pair type, which is used for pairs of values where the type of the second value depends on the first.

This means "there exists a value of type , and a value that depends on with type ".