\( \DeclareMathOperator{\term}{term} \DeclareMathOperator{\wff}{wff} \newcommand{\ove}[2]{{\genfrac{}{}{0.5pt}{0}{#1}{#2}}} \)

\(\lambda\) Logic, Types, Functionality

To and beyond



Type systems I : Introduction & simple systems

Mar 18, 2019

To understand all concepts used in this text, it’s recommended to read this previous article.

Introduction

Types are an important part of most modern programming languages. They serve useful purposes: mainly ensuring a program’s correctness to a certain grade and increasing readability. Many tend to ignore type systems and just take them as given, despite their importance and mathematical background. This series is an attempt at creating awareness about type systems and encouraging the readers explore the possibilities they offer.

On the Notion of Types

To get a use from type systems, it is necessary to think about the concept of types themselves. Even though most systems differ in a lot of aspects, all of them share a few similarities:

Still, you might have one unanswered question: What is a type?

However, it is unexpectedly difficult to find the right definition for the concept, since types itself define concepts for their elements. A generally valid, yet vague explanation would be that every well-formed term has a type and operations are restricted by those types.

A very basic type system

Let’s just take a look at a basic example now, using natural numbers and pairs of them as terms. First, let’s define the possible terms (note that they don’t belong to any types yet): \[ \newcommand{\ove}[2]{{\genfrac{}{}{0.5pt}{0}{#1}{#2}}} \begin{gather} \operatorname{term} 0 \\[8pt] \operatorname{term} n \over \operatorname{term}\, (S\, n)\\[8pt] \operatorname{term} n \qquad \operatorname{term} m \over \operatorname{term} \{n,m\} \\[8pt] \operatorname{term} t \over \operatorname{term} (\operatorname{sum} t) \end{gather} \]

Those are very simple rules for forming numbers, pairs of terms, and applicating the function-like \(\operatorname{sum}​\) on them. Note that I use curly braces for pairing, to avoid confusion with application. Like this, we can prove that obs like \((\mathrm{sum} \{(S\,(S\, 0)), 0\})​\) are indeed terms: \[ \ove{ \ove{ \ove{ \ove{\term\,0}{\term\,(S0)}} {\term\,(S(S0))}\qquad\ove{}{\term\,0}}{\term\,\{(S(S 0),0\}}}{\term\,(\mathrm{sum}\,\{(S\,(S\, 0)), 0\})} \notag \]

However, as mentioned before, some of these terms don’t carry meaning at all and thus can not be typed. Take \((S\{0,0\})\) as an example. What is the successor of a pair of numbers? It simply is useless and thus should not get a way to be typed, as you’ll see.

Just for convenience, rules \(n,m,t\) will be variables standing for terms (for obs \(x\) such that \(\operatorname{term} x\)) from now on. Those are the typing rules of our minimal system (they usually get names): \[ \DeclareMathOperator\term{term}\newcommand\bN{\mathbb{N}} \begin{gather} 0 : \mathbb{N} \tag{$\mathbb{N}$-I1}\\[8pt] n : \bN \over (S\,n) : \bN \tag{$\bN$-I2}\\[8pt] n : \bN \qquad m : \bN \over \{n,m\} : \mathrm{natpair} \tag{natpair-I}\\[8pt] p : \mathrm{natpair} \over (\mathrm{sum}\, p) : \bN \tag{natpair-E} \end{gather} \]

Those rules look quite simple, and they are. The colon denotes the typing relation: \(x : T\) expresses that \(x\) is a member of the type \(T\). Most languages write application of function-likes f(x,y), we’ll write it \(((f x) y)\) or just \(f\, x\, y​\) as many functional programming languages do.

We are only using two types here: natural numbers and pairs of them. As usual in foundational mathematics, the natural numbers start at zero and are defined inductively by defining the base, zero, and a recursion step, the successor constructor (You might call it a function, but neither have we defined the concept of functions, nor would they be real functions when introduced).

Pairs simply rely on their component being numbers using a single constructor that, well, resembles pairs. \(\mathrm{sum}​\) takes a pair to a number. It is the only thing that actually will get changed/eliminated during reduction, and because of this, we will refer to it as a operation.

Also, you might have seen that our pairs aren’t “real”: they have no projections that could let us recreate the individual components. We can only get the components’ sum, therefore we lose information when creating pairs.

Another obvious and quickly thought out, yet extremely important point is that untypeable terms exist as mentioned before.

Proof:

Let \((S\, \{0,0\})​\) be our untypeable term. Because there is only a finite number of rules, we can inductively see none of them applies.

  1. \(\bN​\)-I1 doesn’t apply.

    Proof: obvious.

  2. \(\bN\)-I2 neither applies.

    Proof: For that, we needed to prove \(\{0,0\}\) is a natural number. This proof is obviously impossible, since no conclusion of the form \(\{x : \bN\) can be found, where \(x\) is any ob.

  3. natpair-I doesn’t apply. Proof: \((S \{0,0\})​\) doesn’t start with a curly bracket.

  4. natpair-E doesn’t apply. Proof: \((S \{0,0\})\) doesn’t start with \(\mathrm{(sum}\).

A proof of this kind is elementary and will occur as long as its necessity can be justified by the amount of rules/the required space.

Reduction

Since type theory is not only about logic, but also about programming languages, reduction is the next essential relation to establish, since without it, any kind of use as programming languages can be immediately disregarded because of the inability to run programs. For our system, a reduction relation consists only of a few simple rules.

\[ \newcommand\reduces{\blacktriangleright} \begin{gather} 0 \reduces 0 \tag{red-0}\\[8pt] x \reduces y \qquad y \reduces z \over x \reduces z \tag{red-trans}\\[8pt] x \reduces x' \qquad y \reduces y' \over \{x,y\} \reduces \{x',y'\}\tag{red-pair}\\[8pt] x \reduces x' \over (S x) \reduces (Sx')\tag{red-S}\\[8pt] (\mathrm{sum} \{0,x\}) \reduces x \tag{red-sum-0}\\[8pt] (\mathrm{sum} \{(S x), y\}) \reduces (S(\mathrm{sum} \{x, y\})) \tag{red-plus-S} \end{gather} \] Reflexivity and transitivity are important parts of every reduction relation, since reflexivity makes the relation suitable for a non-strict inequality, and transitivity lets us go further than one step of reduction. Reflexivity is obviously only indirectly given using the invariance rules and (red-0). Another important property is invariance for data constructors.

This is established by (red-pair) and (red-S) which let the reduced version of a compound piece of data (like a pair) be the corresponding constructor applied on the reduced data. Like this, “inner values” always get evaluated first. This tactic is called eager (or strict) evaluation. It is used by most imperative languages, since they mostly rely on data being evaluated in one specific order. The contrasting strategy is called lazy evaluation. Here, values get computed as needed by elimination rules, such that terms “stay unreduced” as long as possible. This tactic has some advantages in computing, like being able to cancel whole expressions. Evaluation will be a much larger topic later on, when discussing theories that could be used as actual programming languages.

Another important term to define is the canonical/normal form: It’s the form in which a term cannot be reduced further and where it’s only composed out of the basic data constructor. Formally, a term \(x\) is in normal form if \(x \reduces y\) implies \(y \equiv x\), where \(\equiv\) is syntactic identity. This is essentially what things actually get computed down to, as we’ll see in the Prolog implementation shown later.

Equality

So, what is left to do? We have defined typing and reduction, now incoming is equality. In order to accomplish this, let us just take a look at the important properties of equality.

However, we won’t be defining the relation from scratch, but rather take convertibility as equality: $$ \[\begin{gather} { \genfrac{}{}{2pt}{}{x \reduces z \qquad y \reduces z}{x = y}} \tag{eq-I1} \end{gather}\] The thick bar means the inference rule is derivable in both directions such that, when being able to in infer the original conclusion and one of the premises, the other is also true. So if we can find a way to reduce two terms to a common form, we know they are equal in some way or another. For example, we can prove that \((\mathrm{sum}\{(S 0), (S(S 0))\})\) and \((\mathrm{sum}\{(0, (S(S(S0))))\})\) are indeed equal. The proof for the premises is left to the reader. This definition are unexpectedly strong: not only identical/renamed terms are considered equal, all terms with the same meaning (the same canonical form) are equal per definition. We could now prove the properties of equality, but in this case it’s just tedious and quite obvious.

Implementation

The implementation is written in Prolog, a language as suitable as possible. Prolog allows us to write rules as we did, yet with a bit more of syntactic clarity. The Prolog interpreter is not only able to check whether a statement is true or not, it is also able to infer terms for which statements are right, e.g. find all \(x\) such that \(x \reduces (S 0)\).

All differences between Prolog and the notation we’re used to are explained within the source code that can also be run online:

SWI-Prolog online

Summary

In this entry, the importance of types was explained, while their universal properties were highlighted. Also, an extremely simple type system got shown, which was used to derive the fundamental relations: typing, reduction and equality. Yet, there are extremely many topics to cover soon, since type systems are way more expressive than most would imagine.