Programming Language Design 2

Extensions to STLC

---

Pairs

You may recall that there are two kinds of algebraic data types, product types and sum types. The simplest interesting product type is a product type of two elements, a pair.

Let’s use the syntax to denote a pair. Here and are the Terms stored within the pair and and are their types. We express the product type of the entire pair with .

Some example of valid pairs could include:

Working with pairs

Being able to define pairs with the (a, b) notation is nice but it’s not very useful as we’ve not yet defined a way to extract the values from the pair. Let’s define the projection functions (surjections) fst and snd that extract the first and second value of the pair respectively.

Using them in our language would look like this:

Now that we’ve sketched out the features of pairs, we are ready to introduce their evaluation rules.

Dynamics of pairs

A pair is considered to be a value if both of its members are values, i.e. . If a pair is not a value, it can be reduced.

The pair can be reduced in two ways; either by reducing its first element or then by reducing its second element. Therefore we can represent the evaluation rule for pairs as follows:

Reduction of fst and snd is a bit more complicated but not unreasonable. The important part about their rules is that the rule for extracting an element from the pair requires the pair to be a value.

Statics of pairs

In STLC, the statics of data types generally consist of two rule sets. The rule sets are the introduction and elimination rules. Such is the case also for the pair.

Introduction rules

In the case of pairs, we only have one introduction rule, since there’s only one way to construct the data type.

Elimination rules

There are two ways to deconstruct a pair and therefore also two elimination rules

Now that we’ve formally defined how a pair would look like in our STLC, let’s try implementing it.

Loading Exercise...

Lists

Another, very interesting, special case of an ADT is the list. Unlike the pair, the list has two data constructors cons and nil. To make the life of our type checker (and our own life implementing it easier) we’ll have the nil constructor take a type as a parameter. In this way, typing nil, and therefore the entire list, becomes a trivial exercise in recursion. Let’s define the behavior for our list constructors as follows:

Above, we use the letter to refer to any type internal to the language, i.e. number, boolean, arrow, pair or list type. As expected, in the refers to the same, although arbitrary, type.

Examples of list declarations:

Similarly to pairs, lists also need deconstructors in order to be useful. In order to be distinguishable from more general ADTs, we call our list deconstruction expression lcase (short for list-case). We’ll define the syntax for it as follows:

An example usage of the lcase in the form of an implementation for head_or_zero:

Dynamics of Lists

Now that we’ve introduces the syntax, let’s take a look at the evaluation rules for lists.

A List is considered a value if it is nil or if both its head and tail is a value, i.e.

Similarly to pairs, we only deconstruct lists that are values, therefore the evaluation rules for lcase are:

The most interesting one, is LCaseCons, where we substitute in the values vh and vt to the term .

Statics of Lists

Similarly to pairs, the typing rules for lists are also split into introduction and elimination rules. The List is in a sense the opposite of a pair because it has two introduction rules and only one elimination rule.

Introduction rules

As mentioned earlier the nil constructor takes the type as an argument in order to make typing it as easy as possible. If this weren’t the case, figuring out the type of nil would be difficult but not impossible¹.

Elimination rules

One key consideration of the lists evaluation rule is the fact that both and have to be of the same type. This is because of the same reason that both branches of an if-then-else have to be of the same type.

Loading Exercise...

Sums

Sums (aka. coproducts) are types that can hold one of two types of values. We used to denote the products so let’s use for sums.

We’ll define the following syntax for constructing sums: and . Notice that similarly to nil, the sum constructors require the type of the other element in the sum. Some examples of sums:

Similarly to lists, deconstructing sums is also done with a case expression:

The names and are short for injection left/right. In fact, like and for pairs are surjections, these functions are injections.

Notice that the syntax for matching sums is very similar to lists. In fact, we could even change lcase to case without ambiguity.

Algebraic data types can share a common syntax for pattern matching, as the constructors in the patterns uniquely determine the type of the subject. This is a common pattern in functional programming languages, such as Haskell.

Here it’s clear that must be a list.

Here it’s clear that it must be a sum type

If there’s a data type called with constructors , here must be a traffic light.

Dynamics of Sums

As one might expect, a sum is considered a value if it contains a value, therefore:

The evaluation rules for sums are very similar to lists and pairs

We reduce the sum until its a value and after that we evaluate the case and substitute the deconstructed value into body of the case.

Statics for Sums

Similarly to Lists, Sums also have two introduction rules and only one elimination rule. Notably, providing the other summands type as an argument to the constructors helps us out a lot.

Introduction rules

Elimination rules

Similarly to the lcase, the bodies of both branches have to be of the same type.

Loading Exercise...

Footnotes

Footnotes

1. In polymorphic type systems nil could be typed as . Type inference for this polymorphic type is always decidable as the type is of rank 2. Types of higher-rank, e.g. don’t have a decidable type inference algorithm for generic type .

   Read more in this Wikipedia article on polymorphism. ↩