Type Theory is a language. We have taken an immersion learning approach to it (as well as to the language of sets) - where we learn a language by listening to it being spoken, relating to known languages and eventually learning the specific idioms. In this note we take a more formal view, looking more explicitly at the rules of the grammar. Hopefully this will complement immersion learning.
In the flavour of type theory we consider, namely Martin-Löf Type Theory (MLTT), all types are of one of the following forms.
Type - these are predefined.We have seen several examples of inductive types. Here we see a little more precisely how to define an inductive type.
We begin with a high-level view of inductive types. All this will become clearer when we see examples.
When defining an inductive type (or later an inductive type family) $W$, we
Type, but for inductive type families we can have other types.Once we define such an inductive type $W$, rules of type theory let us define functions and dependent functions on $W$ by recursion/induction.
We recall an example, binary rooted trees. There are two ways of constructing a binary tree:
We can model this as an inductive type. Namely, we simultaneously define
BinTree : Type.BinTree. These are described by giving them names and specifying their types.The idris code is as below.
data BinTree : Type where
Leaf : BinTree
Node : (left: BinTree) -> (right: BinTree) -> BinTree
We have defined an inductive type by naming it and its constructors and specifying the types of the constructors. Once we do so, we have introduced three new terms with names and types specified - BinTree, Leaf and Node. We can use the constructor terms to construct terms of the type BinTree (this is why they are called constructors).
egTree: BinTree
egTree = Node (Node Leaf (Node Leaf Leaf)) Leaf
It is useful to have a second example. Below is the natural numbers as defined in the idris standard library.
Data type Prelude.Nat.Nat : Type
Natural numbers: unbounded, unsigned integers which can be pattern matched.
Constructors:
Z : Nat
Zero
S : Nat -> Nat
Successor
We mentioned earlier that the types of constructors are such that the constructors can be used to form terms of type $W$. Let us call such types constructor-types for $W$. We will not describe constructor-types full generality but describe the basic cases (we have omitted a slightly more complicated way to construct such types). Recursively, a type $T$ is a constructor-type for an inductive type $W$ if
Leaf : BinTree and Z : Nat,$T = A \to T'$ where $T'$ is a constructor-type for $W$ and A is a type that is previously defined (i.e., without defining $W$),$T = W \to T'$ where $T'$ is a constructor-type for $W$.For example the type of $S : Nat \to Nat$ is a constructor type because $T = Nat$ is allowed for a constructor for Nat by the first rule and hence Nat -> T is allowed by the third rule.
For the constructor Node : BinTree -> BinTree -> BinTree, we use the first rule once and the third rule twice.
In addition to rules for constructing inductive types $W$, we have rules that allow us to define functions on these recursively by giving the definitions for all constructors of $W$, in general recursively. We have seen several examples of these, two of which we recall.
numberVertices : BinTree -> Nat
numberVertices Leaf = 1
numberVertices (Node left right) =
(numberVertices left) + (numberVertices right) + 1
fct: Nat -> Nat
fct Z = 1
fct (S k) = (S k) * (fct k)
We can similarly define dependent functions on an inductive type $W$. This is usually called induction rather than recursion. We will see the relation to proofs by induction in another post.
More generally, rather than defining a single inductive type we can define an inductive type family. This is similar to the above, except that the final target of constructors is some specific member of the type family. We have seen two examples - labelled trees and vectors.
Let us first consider the type family LTree : Type -> Type. This is defined as follows.
data LTree : Type -> Type where
LLeaf : (a: Type) -> (label: a) -> LTree a
LNode : (a : Type) -> (left : LTree a) -> (right : LTree a) -> LTree a
For a fixed type, say Nat, LTree Nat : Type is an inductive type with constructors LLeaf Nat and LNode Nat. Such inductive type families are a simple generalization of inductive types, generally called parametrized inductive type families (similar to generics in many programming languages). Thus we have simply introduced a bunch of inductive types rather than
just one.
On the other hand, the case of Vectors is more subtle. To see this, first look at the definition.
*Intro> :doc Vect
Data type Data.Vect.Vect : (len : Nat) -> (elem : Type) -> Type
Vectors: Generic lists with explicit length in the type
Arguments:
len : Nat -- the length of the list
elem : Type -- the type of elements
Constructors:
Nil : Vect 0 elem
Empty vector
(::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
A non-empty vector of length S len, consisting of a head element and the rest of the list, of length len.
infixr 7
The length of a vector is what is called an index, not a parameter. The key difference is that the constructor (::) for vectors of length, say, $7$ involves vectors of length $6$.
As a consequence we cannot make recursive definitions on vectors of a fixed length. Instead we need to simultaneously define a function on vectors of all lengths. For example, consider the append function.
append: (n: Nat) -> (a: Type) -> (x: a) -> Vect n a -> Vect (S n) a
append Z a x [] = [x]
append (S len) a x (y :: xs) =
y :: (append len a x xs)
The function is defined by specifying how to append to the empty vector, and then how to append to a vector of length $n + 1$ in terms of appending to a vector of length $n$. Note that elem for a vector is a parameter, as constructors (and hence recursion) for a fixed type elem (e.g. elem = Nat) are not related to those for vectors with any other element type.