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.
This section is a work in progress.
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
The key difference between using string
in TypeScript and
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
The product type
The sum type
Dependent function types
A Π-type (pronounced "pi-type") is a dependent function type, which generalizes a regular function type like
This means "for every
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