Notes about type theory I've compiled from some recreational reading.

type_theory_notes.md

Type Theory

Type theory is the mathematical and computational study of type systems, like the ones you use in popular programming languages. It can get very abstract, but I believe it offers some useful concepts to take home even for practical language design. In particular, I am interested in contributing to the Godot game engine's scripting language GDScript https://github.com/godotengine/godot/tree/master/modules/gdscript, so I will try to relate the abstract concepts to concrete examples in GDScript where possible.

The following are some notes I've compiled through some self-study that mostly includes skimming Types and Programming Languages by Benjamin C. Pierce https://github.com/MPRI/M2-4-2/blob/master/Types%20and%20Programming%20Languages.pdf, browsing various Wikipedia articles, sessions with ChatGPT, and a few academic articles. I am just an amateur enthusiast, so these notes may have mistakes or misunderstandings.

Properties of type systems

Below are some properties that can be used to describe type systems. I'll try to give examples and non-examples to help explain each one.

Soundness

A type system is sound if every program that passes the type checker will never hit a type error at runtime. It can be quite difficult to prove that a given language's type system is sound for every valid program, but the following langagues feature type systems which are generally considered sound in everyday use:

• Haskell
• OCaml
• Rust
• TypeScript (with strict settings)

In contract, the following languages are not sound:

• Java
• C++
• GDScript

For example, in Java, the following code compiles, but hits a runtime exception:

ArrayList<String> strings = new ArrayList<>();
ArrayList rawList = strings; // raw type
rawList.add(1); // Compiles fine, but breaks type safety
String s = strings.get(0); // Causes ClassCastException at runtime

In GDScript (as of Godot 4.2) the following compiles but errors at runtime:

var names = [&"hi"]
var strings : Array[String] = names

Decidability

A type system is decidable if a type checker can decide whether any program is well-typed or not in finite time. Even if a language is not decidable, type checkers might be able to succesfully type check most practical programs written in the language. Similarly, a language which is theoretically decidable might take extreemly long to type check in practice.

The following languages have decidable type systems:

• Haskell (without certain extensions)
• GDScript

Haskell is carefully engineered to have a powerful, but still decidable type system. On the other hand, GDScript is currently decidable simply because it lacks certain powerful features like generics.

The following languages have undecidable type systems:

• C++
• TypeScript
• Rust

It's hard to come up with a concrete example of a program in say, C++, that is undecidable. However, C++ template metaprogramming is known to be Turing Complete, meaning it's possible in theory to write any computable function in C++ templates. Deciding whether a C++ program that uses template metaprogramming is well-typed is equivalent to the Halting Problem https://en.wikipedia.org/wiki/Halting_problem, which is known to be undecidable. While the following example is decidable, it illustrates how C++ templates can create infinite loops, which are a key ingredient in being Turing Complete.

template<int N>
struct InfiniteLoop {
    typedef typename InfiniteLoop<N + 1>::type type;
};

int main() {
    InfiniteLoop<1>::type a;  // This line will cause infinite recursion at compile time.
    return 0;
}

Subtyping

Subtyping is a formal way of capturing the notion that "a dog is a kind of animal." When paired with polymorphism, the idea the same code can apply to multiple types, a well-defined notion of subtyping can drastically reduce repetitive code. For example, the body of a function get_age(animal), which returns how old an animal is in years, will be exactly the same for an animal and a dog. Subtype polymorphism allows us to use get_age(animal : Animal) on an object of type Dog without having to define an otherwise identical function get_age(dog : Dog).

Unlike the properties discussed in the previous section, which have the same definition no matter which language you are discussing, each language is free to define exactly what it means by "subtype." In fact, some primitive languages don't have any notion of subtyping at all! That said, a carefully constructed notion of subtyping can go a long way in making a language feel consistent and logical. I will summarize the subtype relation Benjamin C. Pierce gives in Types and Programming Languages, with the understanding that it is not the only way to define subtyping, but rather a solid starting point for discussion.

Properties of the subtype relation

The goal of a subtype relation is to provide consistent rules about when a type like Dog can be safely "substituted" for a type like Animal. For substitution to work as expected, the subtype relation should be reflexive and transitive. These properties are best conveyed using a bit of mathematical notation. To denote that some type $T_1$ (e.g. Dog) is a subtype of some type $T_2$ (e.g. Animal), we write

$$T_1 <: T_2$$

The reflexive property means that every type is a subtype of itself:

$$T_1 <: T_1$$

Example: "Animal is a subtype of Animal"

The transitive property means that

$$T_1 <: T_2 \ \mathrm{and} \ T_2 <: T_3 \ \mathrm{implies} \ T_1 <: T_3$$

Example: "Husky is a subtype of Dog and Dog is a subtype of Animal, therefore Husky is a subtype of Animal.

Top and Bottom types

The subtype relation establishes a sort of heirarchy of types. It is natural to wonder whether this heirarchy has a concrete top and bottom. In other words, is there some top type $T_0$ such that for all types $T$,

$$T <: T_0$$

and is there some bottom type $T_\infty$ such that for all types $T$,

$$T_\infty <: T$$

You may wonder why I have chosen to call the top type $T_0$ and the bottom type $T_\infty$ and not the other way around. When one type is a subtype of another, it means that knowing a particular instance belongs to the subtype reveals more information than knowing it belongs to the other type. For example, learning that a creature is a dog tells you more about it than if you just knew it was an animal. In this sense, learning that an instance belongs to the top type $T_0$ reveals $0$ information. In GDScript, and some other langauges, the top type is called Variant. On the other hand, learning something belongs to the bottom type $T_\infty$ reveals "infinite" information in some sense. However, nothing actually caries infinite information. In fact, it can be proven that the bottom type has no inhabitants. Nevertheless, some languages, such as Haskell, do feature the bottom type and use it as a means to represent concepts like unprovable statements or computations which loop infinitely.

Including the top type $T_0$ in a type system generally does not add much complexity, much like how including $0$ in the natural numbers doesn't significantly change their structure. However, including the bottom type $T_\infty$ can lead to some counterinuitive phenomena in much the same way that describing $\infty$ as a number can lead to paradoxes when not handled carefully.

Struct/Record/Product subtyping

Many languages feature some idea of a "product" type, often called a "record" or "struct". For example, we can think of a 2D vector as being composed of two floats called "x" and "y". The notation we will use to describe this 2D vector type $V_2$ is

$$V_2 = \{ x:\mathrm{float}, y:\mathrm{float} \}$$

Similarly, we can write a 3D vector as

$$V_3 = \{ x:\mathrm{float}, y:\mathrm{float}, z:\mathrm{float} \}$$

Now the question arrises, is the 3D vector type a subtype of the 2D vector type? The answer to this question will vary depending on the specific language, but broadly speaking, there are two camps: structural typing and nominal typing.

Structural Typing

If a language uses structural typing, then the question is answered by checking whether the structure of $V_2$ is "compatible" with the structure of $V_3$. It does, infact, because $V_3$ has a member called $x$ which is a subtype of $V_2$'s member called $x$ (remember that a type is considered a subtype of itself) AND $V_3$ has a member called $y$ which is a subtype of $V_2$'s member called $y$. This same logic can be applied recursively to determine for instance that the type

$$M_{2, 2} = \{ x: \{ x:\mathrm{float}, y:\mathrm{float} \}, y: \{ x:\mathrm{float}, y:\mathrm{float} \} \}$$$

representing a $2$ by $2$ matrix is a subtype of $V_2$.

Nominal Typing

If a language uses nominal typing, then the answer depends entirely on whether the programmer explicitely declares $V_3$ as being a subtype of $V_2$. As it stands, $V_3$ is not a subtype of $V_2$ according to a nominal type system. However, we could imagine defining another type $V_3'$ which inherits $V_2$. There doesn't appear to be a standardized notation for such a type, so I'll write this as

$$V_3' = \mathrm{extends}(V_2, {z:\mathrm{float}})$$

A nominal type system would now consider $V_3'$ a subtype of $V_2$.

Structural vs Nominal Typing

One pro of structural typing is that it can make writing generic, reusable code very easy. For example, suppose I have a move_right function which takes a 2D vector and increments its x coordinate. With structural typing, the same function will "just work" on a 3D vector, even if the programmer didn't specify that 3D vectors extend 2D vectors. This aspect of structural typing can be especially helpful when types don't fit naturally in a nice hierarchical tree.

On the other hand, structural typing can make modeling certain type relationships very complicated in comparison to nominal typing. Suppose our program has a Square type and a Rectangle type. We would like to have Square be a subtype of Rectangle as all squares are rectangles. If we model Rectangle as

$$R = \{ \mathrm{length} : \mathrm{float}, \mathrm{width} : \mathrm{float} \}$$

and Square as

$$S = \{ \mathrm{length} : \mathrm{float} \}$$

the rules of structural typing actually imply that $R &lt;: S$, which is the opposite of what we want! It's much easier to correctly model the relationship between squares and rectangles in a nominally typed system because the programmer can explicitly declare it. For example, one might model squares and rectangles in C++ as follows

class Rectangle {
private:
    float length;
    float width;
public:
    virtual float get_length() { return length; }
    virtual float get_width() { return width; }
};

class Square : public Rectangle {
private:
    float length;
public:
    virtual float get_length() override { return length; }
    virtual float get_width() override { return length; }
};

Type variance

Suppose we have established that Dog is a subtype of Animal. Does it follow that the type Array[Dog] is a subtype of Array[Animal]? Is the type of functions mapping Animal to Animal a subtype of functions mapping Dog to Dog? These are the kinds of questions that type variance addresses.

Given some type $T$, there is often a need for related types such as $\mathrm{Array}[T]$ or $T \rightarrow T$. Abstractly, one can create a new type $T'$ from $T$ using a type constructor $C$:

$$T' = C[T]$$

Templates in C++ are a kind of type constructor.

A type constructor $C$ is said to be covariant if for all types $T_1$ and $T_2$,

$$T_1 <: T_2 \ \mathrm{implies} \ C[T_1] <: C[T_2]$$

A type constructor $C$ is said to be contravariant if for all types $T_1$ and $T_2$,

$$T_1 <: T_2 \ \mathrm{implies} \ C[T_2] <: C[T_1]$$

A type constructor which is neither covariant nor contravariant is said to be invariant.

The following sections list some common type constructors and their variance, along with some demonstrative examples. In the examples, I use C++ syntax for concreteness, but they should be understood as psuedo code, not directly as C++ programs because the typing rules of C++ are extreemly complicated and beyond the scope of these notes.

const

const T is covariant in T. It makes a read-only version of T.

Example:

const Dog dog_1;
const Animal animal_1 = dog_1; // works fine: covariant.

const Animal animal_2;
const Dog dog_2 = animal_2; // this is not allowed: not contravariant
dog_2.bark // uh oh, not every animal can bark, type error!

function parameters

$T_1 \rightarrow T_2$ is contravariant in $T_1$.

Example:

void set_animal(Animal p_animal);
void set_dog(Dog p_dog);

Dog dog;
set_dog(dog);
set_animal(dog); // works fine: parameter is contravariant.
Animal animal;
set_animal(animal);
set_dog(animal); // no good: parameter is not covariant.

function returns

$T_1 \rightarrow T_2$ is covariant in $T_2$.

Example:

Animal get_animal();
Dog get_dog();

Animal anim = get_dog(); // works fine: return type is covariant.
Dog dog = get_animal(); // no good: return type is not contravariant.

pointer/reference

Ref T is invariant in T. In C++, Ref T is written *T. For a particular instance, *t means "the value referenced by t" and &t means "the reference to the value t".

Example:

Dog dog_1;
Animal animal_1;
Animal *animal_ref_1 = &animal_1 // Animal reference to Animal value, totally fine.
Dog *dog_ref_1 = &animal_1 // Dog reference to Animal value, not good because not all animals are dogs.
(*dog_ref_1).bark; // uh oh, animal_1 can't bark: reference is not contravariant


Dog dog_2;
Animal animal_2;
Dog *dog_ref_2 = &dog_2; // Dog reference to Dog value, totally fine.
Animal *animal_ref_2 = &dog_2; // Animal reference to Dog value, what could possibly go wrong?
*animal_ref_2 = animal_2; // the referenced value (dog_2) has been replaced with an animal
dog_2.bark; // uh oh, animal_2 can't bark: reference is not covariant.

arrays

Array[T] is invariant in T. This is because an Array is basically a collection of references. A reference is invariant (see above), so naturally a collection of references is also invariant. However, a read-only Array is covariant, much like const discussed above. Similarly, a write-only Array is contravariant, much like function parameters as discussed previously.

Sum/Tagged Union/Variants/Enum subtyping

Some languages feature the idea of a "sum" type, ocassionally called a "tagged union", "variants" or even just "enums". These types represent an instance that could be one of several possibilities. For example, if a function normally returns an integer, but sometimes returns an error value, we can describe its return type as

$$R = \{ \mathrm{val} : \mathrm{int} | \mathrm{err} : \mathrm{error} \}$$

Unlike product types, where the different names can be accessed directly, the data inside a sum type must be unpacked in some way, typically through some kind of case or match statement, and sometimes through the use of the Visitor pattern.

As far as subtyping is concerned, each of the terms in sum type is a subtype. For example,

$$\mathrm{int} <: R$$

and

$$\mathrm{error} <: R$$

Algebraic Typing

The terms "product type" and "sum type" used above suggest that it is possible to perform some kind of arithmetic or algebra with types. An algebraic type system gives precise meaning to statements like

$$T_4 = (T_1 + T_2) * T_3$$

In particular, addition translates to sum types

$$T_1 + T_2 = \{ t_1 : T_1 | t_2 : T_2 \}$$

and multiplication translates to product types

$$T_1 * T_2 = \{ t_1 : T_1, t_2 : T_2 \}$$

The "tags" $t_1$ and $t_2$ in both equations must be distinct, but are otherwise arbitrary. Allowing for addition and multiplation of types makes a type system extreemly expressive.

Gradual Typing

Gradual typing refers to type systems that feature a mix of untyped and typed code. GDScript is a great example of a gradually typed language. These languages allow programmers to start with code that is completely untyped, which is great for rapid prototyping. As a design solidifies, programmers can return to the code and add type annotations to improve confidence and readability.

The Gradual Guarentee

When a language promisses the "gradual guarentee", it guarentees that adding valid types to a valid program will not change its behaviour. Put another way, the only change type annotations are allowed to bring is type errors. If a language upholds the gradual guarentee, the programmer doesn't have to worry that adding types will introduce bugs. In particular, they can be confident that any errors that do arrise from adding type hints come from catching unintended mistakes in the code, rather than some quirk of the type system. Strictly adhereing to the gradual guarentee is admirable, but poses severe constraints on language design.

Consider the following example in GDScript. Suppose we start with some untyped code.

var number = 3
if number / 2 == 1:
    print("hello world")

Running this code will print "hello world" to the console because number / 2 is treated as the integer division 3 / 2, which gives 1.

Suppose we annotate the code with a type hint as follows.

var number : float = 3
if number / 2 == 1:
    print("hello world")

This version of the code will not print "hello world" because now number / 2 is treaded as the float division 3.0 / 2, which gives 1.5.