Type Theory and PL is a way to formalise programs and making connection between programs and mathematical proofs. Even though, through imperative languages and programs, we can’t clearly see the relationship; however, they are closely related. A few examples will be shown in this article.
Prerequisites
PL used in this article (I predict) would mainly be Agda, Coq. Sometimes Haskell and occasionally some imperative languages.
If you don’t know some of them, don’t be panic, I’ll explain the functionality and the correspondence between the functionalities and semantics when new things come out!
When we were dealing with series problems back in high school, we have seen that series were defined inductively: they have a starting case and the rule that we expand the series.
Formally, we call the starting case Base case, and we call the way we expand them inductive case (step). For instance, Fibonacci Sequence is a great example. For this sequence, the base cases are $F_1 = 1$ and $F_2 = 1$; the inductive case is $F_{i}=F_{i-1}+F_{i-2}, i \in \mathbb{N}, i \gt 2$.
This is the basic concept. Having known this, let’s move to the next step.
Instead of focusing on operations, we can also define some structures (or Sets) inductively. Let’s look at a ‘Hello World’ example of PL: how to define Natural Numbers (Set $\mathbb{N}$ or Nat). As we know that natrual numbers start at zero, and then one, two, three, etc, etc. So the base case of defining Set $\mathbb{N}$ is Zero (denoted by $Z$). Then what’s the inductive step? We can see that to obtain one, we plus one to zero, and to obtain two, we plus one to one, etc. Now, we abstract this operation, “plus one,” to a mapping $S : \mathbb{N} \to \mathbb{N}$: we feed a natural number to the mapping and we obtain a new natural number. Then it is clear that the inductive case is “when we get an element from $\mathbb{N}$, we can utilize the mapping to get another element, which is the next natural number greater than the given one.”
Let’s write out the formalisation:
data ℕ : Set where
Z : ℕ
S : ℕ -> ℕ
Note: this is a way to define a Set in language Agda. It means that there are two cases in this Set; the first case is the base case, which is zero; and the second case is the inductive step, where we can derive new elements that belong to Set ℕ
We call S a constructor since S iteself doesn’t belong to ℕ (but we can regard it as a morphism), but we can get an element in ℕ using S.
For instance, according to our definition, we can get 1 through S Z, applying Z to S. Similarly, to get 2, we can do S (S Z), etc.
The second example might be more familiar. When we define a LinkedList, there are usually two fields.
public class ListNode {
private int data;
private ListNode next;
}
public class IntList {
private ListNode head;
}
The connection might not be that clear when writting it in Java, hmmm. How about Haskell?
data Vec a = Empty | Cons a (Vec a)
Here we see that the tail of the list is exposed in the datatype, and it is inductively defined: the base case is Empty and the inductive step is some element of type a concats with the rest of the list.
The reason why it’s not clear in Java is that we wrapped the inductive step inside ListNode, where the tail of the list is.
Try it
Define Vec in Agda.
Did you encountered some difficulties while defining it in Agda? lol. If you did, just skip it, I’ll explain it later :P
Since lists are a little bit complicated, let’s just focus on how we operate natural numbers. Dreaming back to Elementary School!
Lemme paste the definition of Nat here.
data ℕ : Set where
Z : ℕ
S : ℕ -> ℕ
So the very basic operation of naturals is plus. Intuitively, plus is an operation that takes two natural numbers and then returns the result of their sum. From another aspect, we can view it as a function that map two natural numbers to their sum.
_+_ : ℕ -> ℕ -> ℕ
This is a feature of Agda, which allow us to define infix operators using underscores (stands for positions to fill in parameters) and characters.
How do we plus two numbers. Well, human are clever so they skip constructing the whole things. But computers are dumb; we need to split up the cases:
The first case is simple. By definition of addition, 0 plus a number yields the number itself;
To define the evaluation rule for the second case, we need to notice that for a non-zero number, it must be a successor of some number n. We can denote thses numbers as S n. Of course, we don’t care what n is since we ONLY want to show that these numbers are NOT zero. Thus, intuitively definition is that the sum of a non-zero number S n and another number m is the successor of the sum of n and m.
To sum up, we can define addtion as follow:
Z + _ = _
S n + m = S (n + m)
where the underscore has the same function as that in Haskell which stands for wildcard (we don’t care what it is; it can be any natural number).
Try it Out
Define Multiplication
We are familiar with recursion when writing programs. When I was learning to write recursive functions, my teacher told me to split up the program to two parts:
It’s a pretty clear explanation. But now I want to make connections with mathematical proofs, and indeed, they are isomorphic.
Let’s first take a look at how we do mathematical induction.
To form an inductive proof, we need to prove that the base case holds. And then we are to prove that the next step holds (maybe under the assumption that current step holds).
For instance, let’s prove that plus is associative.
Theorem: $\forall n, m , p \in \mathbb{N}, (n + m) + p = n + (m + p) $
Proof:
We prove associativity by induction on n.
Base case: n is zero. Our goal is to prove (0 + m) + p = 0 + (m + p). According to the definition of plus, we get m + p on LHS and RHS. Property holds by reflexivity.
Inductive Step: n is S n'. Our goal is to prove (S n' + m) + p = S n' + (m + p). The induction hypothesis is (n' + m) + p = n' + (m + p) . According to the definition of plus, we get S ((n' + m) + p) on LHS and S (n' + (m + p)) on RHS. According to the induction hypothesis, (n' + m) + p = n' + (m + p), and thus, according to the congurence rule, our goal holds.
$\blacksquare$
This is how we do it in English. It also holds when we are to write a program. To make it simple, let’s take a look at factorial:
int factorial (int n) {
if (n == 0) return 1;
else return n * factorial(n - 1);
}
Here, the first line, n == 0 case is the base case. And when we calculate the factorial of a non-zero number n, we times n with the factorial of n-1. Here, we assume that factorial(n-1) holds, which is the induction hypothesis.
It is more sophisticated when using Agda since it’s a dependently typed language, where we need to do constructive proof while matching the type of RHS with the type signature.