blog-static/content/blog/01_types_basics.md

title	date	tags	series	draft
Everything I Know About Types: Basics	2022-06-30T19:08:50-07:00	Type Systems Programming Languages	Everything I Know About Types	true

{{< katex_component_js >}} {{< bergamot_js_css >}}

It's finally time to start looking at types. As I mentioned, I want to take an approach that draws a variety of examples from the real world - I'd like to talk about examples from real programming languages. Before doing that, though, let's start with a (working) definition of what a type even is. Let's try the following:

A type is a category of values in a programming language.

Values are grouped together in a category if they behave similarly to each other, in some sense. All integers can be added together or multiplied; all strings can be reversed and concatenated; all objects of some class Dog have a method called bark. It is precisely this categorization that makes type systems practical; since values of a type have common behavior, it's sufficient to reason about some abstract (non-specific) value of a particular type, and there is no need to consider how a program behaves in all possible scenarios. Furthermore, since values of different types may behave differently, it is not safe to use a value of one type where a value of another type was expected.

In the above paragraph, I already introduced some examples of types. Let's take a look at some examples in the wild, starting with numbers. TypeScript gives us the easiest time in this case: it has a type called number. In the below code snippet, I assign a number to the variable x so that I can explicitly write its type.

const x: number = 1;

In other languages, the situation is slightly more complicated; it's frequently necessary to distinguish between values that could have a fractional portion (real numbers) and numbers that are always whole (integers). For the moment, let's focus on integers. These are ubiquitous in various programming languages; Java has int:

int x = 0;

Things in C++, C#, and many other languages look very similar. In Rust, we have to make an even finer distinction: we have to distinguish between integers represented using 32 bits and those represented by 64 bits. Focusing on the former, we could write:

let x: i32 = 0;

In Haskell, we can confirm the type of a value without having to assign it to a variable; the following suffices.

1 :: Int

That should be enough examples of integers for now. I'm sure you've seen them in your programming or computer science career. What you may not have seen, though, is the formal, mathematical way of stating that some expression or value has a particular type. In the mathematical notation, too, there's no need to assign a value to a variable to state its type. The notation is actually very similar the that of Haskell; here's how one might write the claim that 1 is a number.

{{< latex >}} 1:\text{number} {{< /latex >}}

There's one more difference between mathematical notation and the code we've seen so far. If you wrote num, or aNumber, or anything other than just number in the TypeScript example (or if you similarly deviated from the "correct" name in other languages), you'd be greeted with an error. The compilers or interpreters of these languages only understand a fixed set of types, and we are required to stick to names in that set. We have no such duty when using mathematical notation. The main goal of a mathematical definition is not to run the code, or check if it's correct; it's to communicate something to others. As long as others understand what you mean, you can do whatever you want. I chose to use the word \(\text{number}\) to represent the type of numbers, mainly because it's very clear what that means. A theorist writing a paper might cringe at the verbosity of such a convention. My goal, however, is to communicate things to you, dear reader, and I think it's best to settle for clarity over brevity.

Actually, this illustrates a general principle. It's not just the names of the types that we have full control over; it's the whole notation. We could just as well have written the claim as follows:

{{< latex >}} \cdot\ \text{nummie}\ \sim {{< /latex >}}

As long as the reader knew that a single dot represents the number 1, "nummie" represents numbers, and the tilde represents "has type", we'd technically be fine. Of course, this is completely unreadable, and certainly unconventional. I will do my best to stick to the notational standards established in programming languages literature. Nevertheless, keep this in mind: we control the notation. It's perfectly acceptable to change how something is written if it makes it easier to express whatever you want to express, and this is done frequently in practice. Another consequence of this is that not everyone agrees on notation; according to this paper, 27 different ways of writing down substitutions were observed in the POPL conference alone.

{{< bergamot_preset name="notation-preset" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" >}} TNumber @ type(lit(?n), number) <- num(?n); {{< /bergamot_preset >}}

{{< bergamot_exercise label="bergamot; tweaking notation" preset="notation-preset" id="exercise-1" >}} Bergamot, the interactive tool I've developed for doing exercises, supports customizing the notation for rules. Try changing the \(:\) symbol to the \(\sim\) symbol (denoted in latex as \sim).

To change the way that rules are rendered, click the "Presentation Rules" tab in the "Rules" section. There will be a lot there: I've added rules for pretty-printing a fair amount of the standard programming languages notation. Scroll down to LatexTypeBin, and change : to \\sim on that line (the extra backslash is to handle string escaping). Now try typing numbers into the input box; you should see something like \(1 \sim \text{number} \) {{< /bergamot_exercise >}}

One more thing. So far, we've only written down one claim: the value 1 is a number. What about the other numbers? To make sure they're accounted for, we need similar rules for 2, 3, and so on.

{{< latex >}} 2:\text{number} \quad 3:\text{number} \quad ... {{< /latex >}}

This gets tedious quickly. All these rules look the same! It would be much nicer if we could write down the "shape" of these rules, and understand that there's one such rule for each number. This is exactly what is done in PL. We'd write the following.

{{< latex >}} n:\text{number} {{< /latex >}}

What's this \(n\)? First, recall that notation is up to us. I'm choosing to use the letter \(n\) to stand for "any value that is a number". We write a symbol, say what we want it to mean, and we're done.

{{< dialog >}} {{< message "question" "reader" >}} Hold on, isn't this a bit circular? We're saying that n ranges over all numbers, and then saying that a number is anything of the form n. A circular definition of this sort doesn't inspire faith in this approach.{{< /message >}} {{< message "answer" "Daniel" >}} You raise a good point. I am not defining n to be "any expression that has type \text{number}"; rather, there are two meanings to the word "number" in use here. First, there's number-the-symbol. This concept refers to the numerical symbols in the syntax of our programming language, like 1, 3.14 or 1000. Such symbols exist even in untyped languages. Second, there's number-the-type, written in our mathematical notation as \text{number}. This is, as we saw earlier, a category of values.

The rule, then, associates with numerical constants in our language (represented by n) the type \text{number}. {{< /message >}} {{< /dialog >}}

Actually, to be extra precise, we might want to be explicit about our claim that \(n\) is a number, rather than resorting to notational conventions. To do so, we'd need to write something like the following:

{{< latex >}} \cfrac{n \in \texttt{Num}}{n : \text{number}} {{< /latex >}}

Where \(\texttt{Num}\) denotes the set of numbers in our syntax (1, 3.14, etc.) The stuff about the line is called a premise, and it's a simply a condition required for the rule to hold. The rule then says that \(n\) has type number -- but only if \(n\) is a numeric symbol in our language. We'll talk about premises in more detail later on.

Having introduced this variable-like thing \(n\), we need to be careful. It's important to note that the letter \(n\) is not a variable like x in our code snippets above. In fact, it's not at all part of the programming language we're discussing. Rather, it's kind of like a variable in our rules.

This distinction comes up a lot. The thing is, the notation we're building up to talk about programs is its own kind of language. It's not meant for a computer to execute, mind you, but that's not a requirement for something to be language (ever heard of English?). The bottom line is, we have symbols with particular meanings, and there are rules to how they have to be written. The statement "1 is a number" must be written by first writing 1, then a colon, then \(\text{number}\). It's a language.

Really, then, we have two languages to think about:

• The object language is the programming language we're trying to describe and mathematically formalize. This is the language that has variables like x, keywords like let and const, and so on.

  Some examples of our object language that we've seen so far are 1 and 2+3. In our mathematical notation, they look like \(1\) and \(2+3\).

• The meta language is the notation we use to talk about our object language. It consists of the various symbols we define, and is really just a system for communicating various things (like type rules) to others.

  Expressions like \(n \in \texttt{Num}\) and \(1 : \text{number}\) are examples of our meta language.

Using this terminology, \(n\) is a variable in our meta language; this is commonly called a metavariable. A rule such as \(n:\text{number}\) that contains metavariables isn't really a rule by itself; rather, it stands for a whole bunch of rules, one for each possible number that \(n\) can be. We call this a rule schema.

Alright, that's enough theory for now. Let's go back to the real world. Working with plain old values like 1 gets boring quickly. There's not many programs you can write with them! Numbers can be added, though, why don't we look at that? All mainstream languages can do this quite easily. Here's Typescript:

const y = 1+1;

When it comes to adding whole numbers, every other language is pretty much the same. Throwing other types of numbers into the mix, we can arrive at our first type error. Here it is in Rust:

let x = 1.1 + 1;
//          ^ no implementation for `{float} + {integer}`

You see, numbers that are not whole are represented on computers differently than whole numbers are. The former are represented using something called floating point (hence the type name float). Rust wants the user to be fully aware that they are adding two numbers that have different representations, so it makes such additions a type error by default, preventing it from happening on accident. The type system is used to enforce this. In Java, addition like this is perfectly legal, and conversion is performed automatically.

double x = 1.1 + 1;

The addition produces a double-precision (hence double) floating point value. If we were to try to claim that x is an integer, we would be stopped.

int x = 1.1 + 1;
//          ^ incompatible types: possible lossy conversion from double to int

If we tried to save the result of 1.1+1 as an integer, we'd have to throw away the .1; that's what Java means by "lossy". This is something that the Java designers didn't want users to do accidentally. The type system ensures that if either number being added is a float (or double), then so is the result of the addition.

In TypeScript, all numbers have the same representation, so there's {{< sidenote "right" "typescript-no-error-note" "no way to create a type error" >}} Please don't interpret this as praise of TypeScript, or as criticism of other languages. In some languages, it makes more sense to throw type errors in cases like this, while in others it does not. Instead of arguing about some hypothetical "ideal type system", I'd rather explore the various approaches that seem to thrive in the real world. {{< /sidenote >}} by adding two of them.

const x: number = 1.1 + 1; // just fine!

That concludes the second round of real-world examples. Let's take a look at formalizing all of this mathematically. As a starting point, we can look at a rule that matches the TypeScript view of having only a single number type, \(\text{number}\). This rule needs a little bit "more" than the ones we've seen so far; we can't just blindly give things in the form \(a+b\) the type \(\text{number}\) (what if we're adding strings?). For our rule to behave in the way we have in mind, it's necessary for us to add premises. Before I explain any further, let me show you the rule.

{{< latex >}} \frac{e_1:\text{number}\quad e_2:\text{number}}{e_1+e_2:\text{number}} {{< /latex >}}

In the above (and elsewhere) we will use the metavariable \(e\) as a stand-in for any expression in our source language. In general, expressions are things such as 1, x, 1.0+someFunction(y), and so on. In other words, they're things we can evaluate to a value. For the purposes of this article, though, we're only looking at basic types such as numbers and strings, as well as adding them. Thus, at this point, expressions look more like 1, 1+2, "hello"+1. Notice from that last one that expressions need not be well-typed. For the moment, we will avoid rules for checking statements (like let x = 5;).

Rules like the above consist of premises (above the line) and conclusions (below the line). The conclusion is the claim / fact that we can determine from the rule. In this specific case, the conclusion is that \(e_1+e_2\) has type \(\text{number}\). For this to be true, however, some conditions must be met; specifically, the sub-expressions \(e_1\) and \(e_2\) must themselves be of type \(\text{number}\). These are the premises. Reading in plain English, we could pronounce this rule as:

If \(e_1\) and \(e_2\) have type \(\text{number}\), then \(e_1+e_2\) has type \(\text{number}\).

Notice that we don't care what the left and right operands are (we say they can be any expression). We need not concern ourselves with how to compute their type in this specific rule. Thus, the rule would work for expressions like 1+1, (1+2)+(3+4), 1+x, and so on, provided other rules take care of figuring out the types of expressions like 1 and x. In this way, when we add a feature to our language, we typically only need to add one or two associated rules; the ones for other language features are typically unaffected.

Just to get some more practice, let's take a look at a rule for adding strings.

{{< latex >}} \frac{e_1:\text{string}\quad e_2:\text{string}}{e_1+e_2:\text{string}} {{< /latex >}}

This rule is read as follows:

If \(e_1\) and \(e_2\) have type \(\text{string}\), then \(e_1+e_2\) has type \(\text{string}\).

{{< bergamot_preset name="string-preset" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" query=""hello"+"world"">}} TNumber @ type(lit(?n), number) <- num(?n); TPlusI @ type(plus(?e_1, ?e_2), number) <- type(?e_1, number), type(?e_2, number); {{< /bergamot_preset >}}

{{< bergamot_exercise label="bergamot; adding rules for strings" preset="string-preset" id="exercise-2" >}} Try writing the Bergamot rules that correspond to the inference rule for strings above. I've provided the rules for numbers; the rules for strings should be quite similar.

In Bergamot, the claim that an expression e has type t is written as type(e, t). A rule looks like RuleName @ conclusion <- premise1, premise2;. Thus, the rule

TNumber @ type(lit(?n), number) <- num(?n);

Has one premise, that the term \(n\) is a number, and the conclusion is that a number literal has type \(\text{number}\). The num condition is a Bergamot builtin, corresponding to our earlier notation of \(n \in \texttt{Num}\). It holds for all numbers: it's always true that num(1), num(2), etc. The equivalent builtin for something being a string is str.

To edit the rules in Bergamot, click the "Editor" button in the "Rules" section. You will need to add two rules, just like we did for numbers: a rule for string literals (something like \(\texttt{"Hello"} : \text{string}\), but more general) and for adding two strings together. I suggest naming these two rules TString and TPlusS respectively.

When you're done, you should be able to properly determine the types of expressions such as "Hello" and "Hello" + "World". {{< /bergamot_exercise >}}

These rules generally work in other languages. Things get more complicated in languages like Java and Rust, where types for numbers are more precise (\(\text{int}\) and \(\text{float}\) instead of \(\text{number}\)). In these languages, we need rules for both.

{{< latex >}} \frac{e_1:\text{int}\quad e_2:\text{int}}{e_1+e_2:\text{int}} \quad\quad \frac{e_1:\text{float}\quad e_2:\text{float}}{e_1+e_2:\text{float}} {{< /latex >}}

But then, we also saw that Java is perfectly fine with adding a float to an integer, and an integer to a float (the result is a float). Thus, we also add the following two rules (but only in the Java case, since, as we have seen, Rust disallows adding a float to an integer).

{{< latex >}} \frac{e_1:\text{int}\quad e_2:\text{float}}{e_1+e_2:\text{float}} \quad\quad \frac{e_1:\text{float}\quad e_2:\text{int}}{e_1+e_2:\text{float}} {{< /latex >}}

You might find this process of adding rules for each combination of operand types tedious, and I would agree. In general, if a language provides a lot of automatic conversions between types, we do not explicitly provide rules for all of the possible scenarios. Rather, we'd introduce a general framework of subtypes, and then have a small number of rules that are responsible for converting expressions from one type to another. That way, we'd only need to list the integer-integer and the float-float rules. The rest would follow from the conversion rules. Chapter 15 of Types and Programming Languages by Benjamin Pierce is a nice explanation, but the Wikipedia page ain't bad, either.

{{< bergamot_preset name="conversion-preset" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" >}} section "Conversion rules" { ConvertsIS @ converts(integer, string) <-; ConvertsIF @ converts(integer, float) <-; ConvertsFS @ converts(float, string) <-; }

section "Rules for literals" { TInt @ type(lit(?n), integer) <- int(?n); TFloat @ type(lit(?f), float) <- float(?f); TString @ type(lit(?s), string) <- str(?s); }

section "" { TPlusInt @ type(plus(?e_1, ?e_2), integer) <- type(?e_1, integer), type(?e_2, integer); TPlusFloat @ type(plus(?e_1, ?e_2), float) <- type(?e_1, float), type(?e_2, float); TPlusString @ type(plus(?e_1, ?e_2), string) <- type(?e_1, string), type(?e_2, string); }

TConverts @ type(?e, ?tau_2) <- type(?e, ?tau_1), converts(?tau_1, ?tau_2); {{< /bergamot_preset >}}

{{< bergamot_exercise label="advanced; a taste of conversions" preset="conversion-preset" id="exercise-3" >}} This exercise is simply an early taste of formalizing conversions, which allow users to (for example) write numbers where the language expects strings, with the understanding that the number will be automatically turned into a string.

To avoid having an explosion of various rules, we instead define the "converts to" relation, \(\tau_1 \preceq \tau_2\), where \(\tau_1\) and \(\tau_2\) are types. To say that an integer can be automatically converted to a floating pointer number, we can write \(\text{integer} \preceq \text{float}\). Then, we add only a single additional rule to our language: TConverts. This rule says that we can treat an expression of type \(\tau_1\) as an expression of type \(\tau_2\), if the former can be converted to the latter.

I have written some rules using these concepts. Input some expressions into the box below that would require a conversion: some examples might be 1 + 3.14 (adding an integer to a float), 1 + "hello" (adding an integer to a string), and 1.0 + "hello" (adding a float to a string). Click the "Proof Tree" tab to see how the various rules combine to make the expression well-typed.

Now, remove the ConvertsIS rule that allows integers to be converted to strings. Do all of the expressions from the previous paragraph still typecheck? Can you see why?

{{< /bergamot_exercise >}}

Subtyping, however, is quite a bit beyond the scope of a "basics" post. For the moment, we shall content ourselves with the tedious approach.

Another thing to note is that we haven't yet seen rules for what programs are incorrect, and we never will. When formalizing type systems we rarely (if ever) explicitly enumerate cases that produce errors. Rather, we interpret the absence of matching rules to indicate that something is wrong. Since no rule has premises that match \(e_1:\text{float}\) and \(e_2:\text{string}\), we can infer that {{< sidenote "right" "float-string-note" "given the rules so far," >}} I'm trying to be careful here, since adding a float to a string is perfectly valid in Java (the float is automatically converted to a string, and the two are concatenated). {{< /sidenote >}} 1.0+"hello" is invalid. The task of adding good type error messages, then, is usually a more practical concern, and is undertaken by compiler developers rather than type theorists. There are, of course, exceptions; check out, for instance, these papers on improving type error messages, as well as this tool that showed up only a week or two before I started writing this article.

• Chameleon, a tool for debugging Haskell error messages.
• This paper, titled Type debugging with counter-factual type error messages using an existing type checker.
• Another paper, Compositional explanation of types and algorithmic debugging of type errors.

One last thing. So far, I've been defining what each metavariable means by giving you examples. However, this is not common practice in the theory of programming languages. There is actually another form of notation that's frequently used from defining what various symbols mean; it's called a grammar. A grammar for our little addition language looks like this:

{{< latex >}} \begin{array}{rcll} e & ::= & n & \text{(numbers)} \ & | & s & \text{(strings)} \ & | & e+e & \text{(addition)} \end{array} {{< /latex >}}

This reads,

An expression is a number or a string or the sum of two expressions.

I think this is all I wanted to cover in this part. We've gotten a good start! Here's a quick summary of what we've covered:

1. It is convenient to view a type as a category of values that have similar behavior. All numbers can be added, all strings can be reversed, and so on and so forth. Some types in existing programming languages are the number type from TypeScript, i32 and int for integers in Rust and Java, respectively, and float for real {{< sidenote "right" "float-not-real" "(kinda)" >}} A precise reader might point out that a floating point number can only represent certain values of real numbers, and definitely not all of them. {{< /sidenote >}} numbers in C++.
2. In programming language theory, we usually end up with two languages when trying to formalize various concepts. The object language is the actual programming language we're trying to study, like Python or TypeScript. The meta language is the language that we use to reason and talk about the object language. Typically, this is the language we use for writing down our rules.
3. The common type-theoretic notation for "expression \(x\) has type \(\tau\)" is \(x : \tau\).
4. In writing more complicated rules, we will frequently make use of the inference rule notation, which looks something like the following. {{< latex >}} \frac{P_1 \quad P_2 \quad ... \quad P_n}{P} {{< /latex >}} The above is read as "if \(P_1\) through \(P_n\) are true, then \(P\) is also true."
5. To support operators like + that can work on, say, both numbers and strings, we provide inference rules for each such case. If this gets cumbersome, we can introduce a system of subtypes into our type system, which preclude the need for creating so many rules; however, for the time being, this is beyond the scope of the article.

Next time we'll take a look at type checking expressions like x+1, where variables are involved.

This Page at a Glance

{{< dialog >}} {{< message "question" "reader" >}} Hey, what's this section? I thought we were done. {{< /message >}} {{< message "answer" "Daniel" >}} We are. However, various parts of this series will build on each other, and as we go along, we'll be accumulating more and more various symbols, notation, and rules. I thought it would be nice to provide a short-and-sweet reference at the bottom for someone who doesn't want to re-read the whole section just to find out what a symbol means. {{< /message >}} {{< message "question" "reader" >}} So it's kind of like a TL;DR? {{< /message >}} {{< message "answer" "Daniel" >}} Yup! I also would like to somehow communicate the feeling of reading Programming Languages papers once you are familiar with the notation; after a little bit of practice, you can just read the important figures and already be up-to-speed on a big chunk of the content. {{< /message >}} {{< /dialog >}}

Metavariables

Symbol	Meaning	Syntactic Category
\(n\)	Numbers	\(\texttt{Num}\)
\(s\)	Strings	\(\texttt{Str}\)
\(e\)	Expressions	\(\texttt{Expr}\)

Grammar

{{< block >}} {{< latex >}} \begin{array}{rcll} e & ::= & n & \text{(numbers)} \ & | & s & \text{(strings)} \ & | & e+e & \text{(addition)} \end{array} {{< /latex >}} {{< /block >}}

Rules

{{< foldtable >}}

Rule	Description
{{< latex >}}\frac{n \in \texttt{Num}}{n : \text{number}} {{< /latex >}}	Number literals have type \(\text{number}\)
{{< latex >}}\frac{s \in \texttt{Str}}{s : \text{string}} {{< /latex >}}	String literals have type \(\text{string}\)
{{< latex >}}\frac{e_1 : \text{string}\quad e_2 : \text{string}}{e_1+e_2 : \text{string}} {{< /latex >}}	Adding strings gives a string
{{< latex >}}\frac{e_1 : \text{number}\quad e_2 : \text{number}}{e_1+e_2 : \text{number}} {{< /latex >}}	Adding numbers gives a number

Playground

{{< bergamot_widget id="widget" query="" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" >}} section "" { TNumber @ type(lit(?n), number) <- num(?n); TString @ type(lit(?s), string) <- str(?s); } section "" { TPlusI @ type(plus(?e_1, ?e_2), number) <- type(?e_1, number), type(?e_2, number); TPlusS @ type(plus(?e_1, ?e_2), string) <- type(?e_1, string), type(?e_2, string); } {{< /bergamot_widget >}}