Introduction to Type Theory for Programmers

A program can be thought of as functions. They take some input data and produce some output data. Each value has a type associated with it. 32.1 is a number and "hello!" is a string. Types for the same conceptual value might not be the same in every programming language. In C, C++, Java, and Python, 32.1 is a float. Unlike JavaScript, these languages differentiate between integers and other real numbers.

JavaScript in 111 Seconds

To get on the same page, this post is going to use JavaScript for its examples. If you already know JavaScript and TypeScript, you can skip ahead.

Here are some different types in a few programming languages:

This is not an exhaustive list but it should be enough to get us up and running.

To get familiar with the syntax of JavaScript, I'm going to write the same functions in each of these languages:

function average(a, b) {
   return (a + b) / 2;
}

function exclaim(s) {
   return s + "!";
}

function average(a: number, b: number): number {
   return (a + b) / 2;
}

function exclaim(s: string): string {
   return s + "!";
}

float average(float a, float b) {
   return (a + b) / 2;
}

char *exclaim(char const *s) {
   size_t old_len = strlen(s);
   size_t new_len = old_len + 1;
   char *out = malloc(new_len + 1); // +1 for '\0'
   memcpy(out, s, old_len);
   out[old_len] = '!';
   out[new_len] = '\0';
   return out;
}

float average(float a, float b) {
   return (a + b) / 2;
}

String exclaim(String s) {
   return s + "!";
}

def average(a, b):
   return (a + b) / 2

def exclaim(s: str) -> str:
   return s + "!"

Besides the C one that took some memory finagling, they all more or less look the same. There are two things of note:

1. The TypeScript is almost identical to the the JavaScript. The only difference is types attached using : type.
2. The Python program has types listed for exclaim but not average. That's because average(a: int, b: int) -> float wouldn't quite be accurate. a and b can be either int or float¹.

The rest of this post will use JavaScript (and eventually TypeScript). We won't use advanced syntax in this post.

Dynamic Typing

In dynamically typed languages like JavaScript and Python, you don't always know the type of a variable when you're writing the code.

Let's look at an example program in JavaScript:

function average(a, b) {
   return (a + b) / 2;
}

I can call this function in several different ways:

average(4, 2);         => 3
average(5.5, 4.5);     => 5
average(4, "2");       => 21
average("uh", "oh");   => NaN

Depending on the types of the arguments, something very different happens. Particularly on lines 3 and 4. In JavaScript, when you add two numbers, you get another number. But when you add two strings, you get another string. Additionally, anything plus a string gets you another string. People call this behavior weak-typing².

 1   +  2  == 3
"1"  + "2" == "12"
 1   + "2" == "12"
null + "y" == "nully"

Graduating to Static Typing

We can do better. Let's switch to TypeScript and start adding types to our arguments. We'd like to prohibit inputs that make the function behave strangely.

1
function average(a: number, b: number): number {
2
   return (a + b) / 2;
3
}
4

5
average(4, "2");
6
average("uh", "oh");

Argument of type 'string' is not assignable to parameter of type 'number'.

As desired. In this case, we used types to constrain the function domain, thereby shrinking the program execution space to something more representative of "average". A smaller execution space is easier to reason about.

With static typing, we can catch rare bugs:

1
let x;
2
if (Math.random() > 0.001) {
3
   x = average(9, 9);
4
} else {
5
   // very rare!
6
   // compiler catches the bug anyways
7
   x = average("9", 9);
8
}

Easing Into Math

Our next code sample is rather contrived:

1
function times_two(x: number): number {
2
   const y = Math.floor(x) * 2;
3
   if (y % 2 === 0) {
4
      return y;
5
   }
6

7
   //return
8
}

Function lacks ending return statement and return type does not include 'undefined'

We, as humans, know that y is always an integer multiple of 2. y modulo 2 must be 0. Unfortunately, TypeScript isn't that clever yet.

Let's try and talk about that in a more mathematical way. The primary motivation for math in this case is terseness, formality, and precision. To do that, we'll need to briefly cover logic and set theory. If you know these, you can skip ahead.

• Logical Connectives
  • Not: $\neg$
  • And: $\land$
  • Or: $\lor$
• Quantifiers
  • Exists: $\exists$
  • For All: $\forall$
• Misc
  • Such That: $\text{st}$ or $\ni:$
  • Therefore: $\therefore$

Sets are pretty great. They're similar to arrays or lists in that they contain elements, but a set cannot have duplicate elements. A value is either in a set or it isn't. Unlike a list, the order of elements within a set does not matter.

A set is written using braces. The following are sets containing only 1, 2, and 3 and they are all equivalent:

• $\{1, 2, 3\}$
• $\{1, 2, 3, 1\}$
• $\{3, 2, 1\}$

To write "a is an element of A", we write $a\,\in\,A$.

You can also construct sets using other sets. The syntax is $\{\textit{value}\,|\,\textit{conditional}\}$. For example:

$$ \begin{align} \text{let}\,A &= \{1, 2, 3\} \\ B &= \{2 * a\,|\,a\in A\} \\ B &= \{2, 4, 6\} \end{align} $$

There are also some common set names:

• Empty Set: $\text{Ø}$
• Real Numbers: $\mathbb{R}$
• Integers: $\mathbb{Z}$
• Positive Integers (Natural Numbers): $\mathbb{N}^+$

function times_two(x: number)

   const y = Math.floor(x) * 2;

   if (y % 2 === 0) {
      return y;
   }

Was this argument convincing? I think it was. But there's a huge problem: we had to use our brain. Brains can make mistakes and can be convinced of things that are untrue so this proof is ungood.

Assembling a Type Theory

It'd be just great if we could mechanize this process. Once again, I will introduce more notation³:

$$ \frac{\textit{Premise}_1\quad...\quad\textit{Premise}_n}{\textit{Conclusion}}\textit{Name} $$

This is no fraction! This is an inference rule. Let's look at a few examples:

From these rules, I can prove that if it is raining and I have flowers in my garden, then my flowers are watered.

$$ \frac{\dfrac{\text{Raining}}{\text{Wet In My Garden}}\quad\text{Flowers in My Garden}}{\text{Flowers Watered}} $$

Also, if we can prove something without a premise, we simply omit the premises entirely:

$$ \frac{}{\text{Types Are Wonderful!}} $$

Fun, right? Let's get some type theory going by writing inference rules for the JavaScript + operator.

First, recursively define JavaScript expressions and create notation:

• $n$ is any $\mathbb{R}$
• $s$ is any string
• $e$ is an expression, which is one of:
  • $n$
  • $s$
  • $e_1 + e_2$

Subscripting any of these just distinguishes them. $n_1$ and $n_2$ are both Reals, but not necessarily the same one.

Here are some JavaScript expressions written out in symbols:

For clarity, let's always use brackets around the whole expression.

Next, let's define our types.

• $\diamond$ (diamond)
• $\omega$ (omega)
• $\tau$ (tau) is a type, which is one of:
  • $\diamond$
  • $\omega$

Now, I'm not going to tell you what $\diamond$ and $\omega$ are but I will show you how they're used.

Recall the rules of the JavaScript + operator:

number + number => number
string + any    => string
any    + string => string

Try to understand the notation and guess what $\diamond$ and $\omega$ mean. Then open the answer below.

Functions, Variables, and Context! Oh My!

What about functions and variables? For those, we will have to extend both the JavaScript expression grammar and the type grammar:

• $n$ is any $\mathbb{R}$
• $s$ is any string
• $v$ is a variable, which is one of: ‼️
  • $x$
  • $y$
  • $z$
• $e$ is an expression, which is one of:
  • $n$
  • $s$
  • $v$
  • $e_1 + e_2$
  • $v \Rightarrow e$ is a lambda‼️
  • $e_1(e_2)$ is a lambda call‼️
• $\diamond$ is any number
• $\omega$ is any string
• $\tau$ is a type, which is one of:
  • $\diamond$
  • $\omega$
  • $\tau_1 \rightarrow \tau_2$ is a function from $\tau_1$ to $\tau_2$‼️

"Wait, where are the functions I was promised?", you ask.

Instead of functions, we're going to have lambdas⁴. They work like so: $\textit{Parameter Name} \Rightarrow \textit{Return Expression}$

function add_three(a) {
   return a + 3;
}

// equivalent

add_three = a => a + 3;

Now consider the following program:

$$ [(x \Rightarrow x + 1)(2) + (x \Rightarrow x + 1)(\textcolor{green}{\texttt{"2"}})] $$

What is the type of $[x + 1]$? Well, that depends on the context, doesn't it?

But this notation only allows us to have one type for $x$. We'll have to think differently now.

Introducing $\Gamma$ (Gamma), the type context! Think of it like a dictionary of resolved types for variables⁵.

Γ = {v1: 𝜏1, v2: 𝜏2, ...};

When I write $\Gamma \vdash [x] : \tau$, read "In a certain context $\Gamma$, $x$ has type $\tau$"⁶.

Let's update our inference rules.

There are two brand new rules. I would encourage you to try and work them out on your own and then check your understanding below.

Thank you for reading and happy typing!

I;m Thinking About Thos Types :)

Citations

1. F. Shinko, Introduction to type theory. [Online]. Available: https://math.berkeley.edu/~forte/notes/type_theory.pdf. Accessed: Mar. 12, 2025.
2. H. Geuvers, Introduction to Type Theory. [Online]. Available: https://www.cs.ru.nl/~herman/onderwijs/provingwithCA/paper-lncs.pdf. Accessed: Mar. 13, 2025.
3. B. C. Pierce, Types and Programming Languages Cambridge, MA, USA: MIT Press, 2002.

Footnotes