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.
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.
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 runtimeIn GDScript (as of Godot 4.2) the following compiles but errors at runtime:
var names = [&"hi"]
var strings : Array[String] = namesA 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 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.
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 Dog) is a subtype of some type Animal), we write
The reflexive property means that every type is a subtype of itself:
Example: "Animal is a subtype of Animal"
The transitive property means that
Example: "Husky is a subtype of Dog and Dog is a subtype of Animal, therefore Husky is a subtype of Animal.
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
and is there some bottom type
You may wonder why I have chosen to call the top type Variant. On the other hand, learning something belongs to the bottom type
Including the top type
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
Similarly, we can write a 3D vector as
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.
If a language uses structural typing, then the question is answered by checking whether the structure of
representing a
If a language uses nominal typing, then the answer depends entirely on whether the programmer explicitely declares
A nominal type system would now consider
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
and Square as
the rules of structural typing actually imply that
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; }
};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
Templates in C++ are a kind of type constructor.
A type constructor
A type constructor
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 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!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.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.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.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.
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
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,
and
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
In particular, addition translates to sum types
and multiplication translates to product types
The "tags"
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.
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.