We sketch an introduction to the concepts of dependent type theory accompanied by idris code. This note does not include propositions as types, which will be in the sequel. This is an annotated version of the live code from the lecture but wih some reordering for a better flow.
Objects in type theory are called terms. Each term has a type, generally unique. The notation a: A means a is a term of type A.
For example Nat is a type and we define a term three of type Nat. Note that in idris we must specify the type of a term being defined
before defining it.
three : Nat
three = 3
The next term we define is a function. Observe that its type is the function type Nat -> Nat. A function is just a term whose type is a
function type.
next : Nat -> Nat
next n = n + 1
We can apply a function to a value in its domain. For example, we see:
*Intro> next 3
4 : Nat
Function types are central to functional programming. In mathematics and programming, one also considers functions of more that one variable. However we can instead use a tricj called Currying to define iterated functions.
add : Nat -> Nat -> Nat
add m n = m + n
This means, for example, that add 3 is the function given by adding 3. We see:
*Intro> add 2
add 2 : Nat -> Nat
*Intro> add 2 3
5 : Nat
A very important way to define functions is recursively, i.e., a function f is defined by specifying f(n) in terms of other values f(m).
A specific kind of recursion is primitive recursion. For functions on natural numbers this means that we define f(0) as a constant (i.e. without using f in the rhs) and define
f(n + 1) in terms of f(n) only.
fct: Nat -> Nat
fct Z = 1
fct (S k) = (S k) * (fct k)
We see:
*Intro> fct 5
120 : Nat
An important feature of primitive recursion is that the definitions are guaranteed to terminate for all inputs, i.e. the functions are total.
Indeed this can be checked by idris.
*Intro> :total fct
Intro.fct is Total
For contrast, consider the following function. It is easy to see that trying to calculate loop 1 runs forever.
loop: Nat -> Nat
loop Z = Z
loop (S k) = loop k + (loop (k + 2))
Naturally, idris is suspicious.
*Intro> :total loop
Intro.loop is possibly not total due to recursive path:
Intro.loop, Intro.loop, Intro.loop
In our next example, we define Fibonacci numbers. The usual definition of these, fib(n + 2) = fib(n + 1) + fib(n) is not primitive recursive.
Instead we use a trick, giving a primitive recursive definition of $n\mapsto (fib(n), fib(n+1))$ and define fibonacci numbers in terms of this.
Note that the codomain of fibPair is the product type (Nat, Nat) = Pair Nat Nat.
fibPair: Nat -> (Nat, Nat)
fibPair Z = (1, 1)
fibPair (S k) = case fibPair k of
(a, b) => (b, a + b)
fibo: Nat -> Nat
fibo n = fst (fibPair n)
We see:
*Intro> map fibo [0..10]
[1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89] : List Nat
Before we move on, some remarks about recursion.
An inductive type is a type defined by defining introduction rules that are the ways a term of the type can be constructed.
For instance a binary tree is either a leaf or a node where two binary trees are joined. This can be defined in idris
using a data definition (the name comes from datatype)
data BinTree : Type where
Leaf : BinTree
Node : (left: BinTree) -> (right: BinTree) -> BinTree
An example is as follows.
egTree: BinTree
egTree = Node (Node Leaf (Node Leaf Leaf)) Leaf
As we have mentioned before, we can define functions recursively on inductive types. The following counts the number of vertices.
numberVertices : BinTree -> Nat
numberVertices Leaf = 1
numberVertices (Node left right) =
(numberVertices left) + (numberVertices right) + 1
We see:
*Intro> numberVertices egTree
7 : Nat
The above was functional programming, not yet dependent type theory. In Dependent Type Theory, a type is a term, i.e. an object. Specifically,
Type in idris)First let us assign some types to variables.
Naturals : Type
Naturals = Nat
natToNat : Type
natToNat = Nat -> Nat
Note that as Naturals and Nat are equal, 3 has type Naturals
anotherThree : Naturals
anotherThree = 3
We can generalize inductive types to inductive type families. Rather than defining a single inductive type, we define a family of them.
A simple example of this is binary trees with leaves labelled. The labels can have any type a, but all labels should have the same type.
We view this as a function that given a type has value a type. Functions with values that are types are called type families.
data LTree : Type -> Type where
LLeaf : (a: Type) -> (label: a) -> LTree a
LNode : (a : Type) -> (left : LTree a) -> (right : LTree a) -> LTree a
Here is an example
egLTree : LTree Nat
egLTree =
LNode Nat (
LNode Nat (LLeaf Nat 1) (LNode Nat (LLeaf Nat 3) (LLeaf Nat 4))
) (LLeaf Nat 7)
Here too we can define functions by recursion.
labels : (a: Type) -> LTree a -> List a
labels a (LLeaf a label) = [label]
labels a (LNode a left right) =
(labels a left) ++ (labels a right)
We see:
*Intro> labels _ egLTree
[1, 3, 4, 7] : List Nat
Remark: The type LTree a depended on the type a, not say a natural number. Such dependence is possible, and indeed common,
even in languages where types are not objects. For example we have List[A] in scala or List<A> in java. We will soon see genuine dependent types.
$\Pi$-typesWe now define a type family with domain Nat, i.e. a function Nat -> Type. This is the type of tuples.
We can view tuples as given recursively. To do this we use the Unit type - this is a type with just one term, denoted ()
Unit.We define the type of $n$-tuples as a function of $n$ recursively. This is thus a type family.
Tuple: Nat -> Type -- tuples of Natural numbers
Tuple Z = Unit
Tuple (S k) = (Nat, Tuple k)
Now we can define concrete $n$-tuples and see that they have the expected type.
egTuple : Tuple 2
egTuple = (3, (4, ()))
Better still we can define a term countdown which associates to n the countdown to 1, e.g. countdown 3 is the $3$-tuple
(3, (2, (1, ()))). The definition is recursive.
countdown : (n: Nat) -> Tuple n
countdown Z = ()
countdown (S k) = (S k, countdown k)
We see:
*Intro> countdown 3
(3, 2, 1, ()) : (Nat, Nat, Nat, ())
While the above looked innocuous, note that the type of countdown n is Tuple n, which is not fixed. Thus countdown is not a function
in the usual sense (like say Fibonacci numbers) with fixed domain and codomain. Instead, while the domain is indeed a fixed type Nat,
the type of the values depend on the arguments.
Such functions are called dependent functions. The type of such a functions is called a dependent function type or a $\Pi-type (
the latter term is because they are in some sense products). For instance in more mathematical type theory notation,
$$countdown : \prod_{n\in \mathbb{N}} Tuple(n)$$
A much better way to define vectors is as an (indexed) inductive type, similar to how we defined BinTree and LTree
(we note a key difference later).
Here is the idris documentation for vectors.
*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
We have a different version of countdown, giving vectors and counting down to $0$. Note the type involves S n to get the correct length.
cntd : (n: Nat) -> Vect (S n) Nat
cntd Z = [0]
cntd (S k) = (S k) :: (cntd k)
We see:
*Intro> cntd 4
[4, 3, 2, 1, 0] : Vect 5 Nat
Next, a more practically useful example. When we zip two lists, it is generally an error if they do not have the same length. With dependent types, we can enforce this as part of the syntax.
zipNat : (n: Nat) -> Vect n Nat -> Vect n Nat -> Vect n (Nat, Nat)
zipNat Z [] [] = []
zipNat (S len) (x :: xs) (y :: ys) = (x , y) :: (zipNat len xs ys)
We see:
*Intro> zipNat _ [1, 3, 5] [10, 20, 30]
[(1, 10), (3, 20), (5, 30)] : Vect 3 (Nat, Nat)
A couple of more examples: zipping vectors of arbitrary types and appending to a vector. Note the signatures.
zip : (n: Nat) -> (a: Type) -> (b: Type) -> Vect n a -> Vect n b -> Vect n (a, b)
zip Z a b [] [] = []
zip (S len) a b (x :: xs) (y :: ys) =
(x, y) :: (zip len a b xs ys)
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)
$\Sigma$-typesFor the final concept of this post, we consider how we could define a filter function on vectors, which, for example, returns all the prime numbers in the vector. The subtlety is that the length of the vector, and hence the return type, is not determined by the argument type.
What we do is return a pair $(m, v)$ where $m$ is a natural number and $v$ is a vector of length $m$. Note that this is not
an ordinary pair, i.e. of the form $(a, b) : A \times B$ with $a: A$ and $b: B$, since the type of the second component $v$
depends on the first component $m$. Such a pair is called a dependent pair and its type a dependent pair type or a $\Sigma$-type.
More generally, let $A$ be a type and $B: A\to Type$ be a type family. We then can form the $\Sigma$-type
$$\sum_{a\in A} B(a)$$
with terms of this type pairs $(a, b)$ with $a : A$ and $b: B(a)$. In idris the notation ** is used to denote dependent pair types
as well as dependent types.
filter: (n: Nat) -> (a: Type) -> (p: a -> Bool) -> Vect n a -> (m: Nat ** Vect m a)
filter Z a p [] = (Z ** [])
filter (S len) a p (x :: xs) =
(case p x of
False => filter len a p xs
True => (case filter len a p xs of
(m ** pf) =>
(S m ** x :: pf) ))
An example is as follows. In idris $\lambda$ is denoted by backslash, so \n => n > 2 is the function $n\mapsto n > 2$.
*Intro> filter _ Nat (\n => n > 2) [1, 3, 4, 2, 5]
(3 ** [3, 4, 5]) : (m : Nat ** Vect m Nat)
The first component 3 above is the length of the result and the second component the vector of this length obtained by filtering.
In First-Order Logic we had very few rules for forming expressions: forming recursive terms, atomic formulas, combinations of formulas and quantified formulas. It seems that in type theory, we have a lot of rules. But in fact there are fewer rules than in the examples above, since some of them (such as forming pairs) are special cases of others.
Indeed below is a full list of rules for forming types and terms (though some details of these rules are subtle).
Type.f x = y where y is an expression that can depend on x (this is a $\lambda$ definition).f is a (dependent) function with domain A and a : A we can form the term f a.