Introduction

Here we are again in our mission to understand Agda programming language and how dependent types eases the task of construct correct software. As I have said before, I am basing this tutorial on a Connor McBride’s talk Developing Dependently Typed Programs in LEGO, extending it here or there…

In this post, I will discuss the type of finite sets, a very useful data type. But, first we need to understand what is a dependent type and how it can help us in our task to build better software. To this end, first I will present vectors, or size indexed lists, as they are a cannonical example of dependent types.

Vector as cannonical example of dependent types

Lists are a very useful data type that are part of every functional programmer toolbox. Below is the definition of lists and a function that returns the head of a given list.

data List (A : Set) : Set where
	[] : List A

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A

headList : ∀ {A : Set} → List A → Maybe A
headList [] = nothing
headList (x ∷ _) = just x

Lists are useful, but have some drawbacks. For example, how can we define a head function that exclude applications on empty lists? On languages that do not support dependent types, the solution is use a dummy value to be returned in the case that the list passed as an argument is empty or use a data type like Maybe or Either (Haskell terminology…) that can be used to represent something like exceptions in a pure setting.

The main issue with lists is that its data type definition give us no information on how many elements their values have. To solve this problem, we can use a similar data type, indexed by a natural number that represents the number of elements in the list. We call such type a Vector and its definition is:

data Vec {l}(A : Set l) : ℕ → Set l where
  [] : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

Using type theory terminology, Vector data type defines an indexed type family. This means that for each natural number \(n\) we have a type Vec A n. Note that, unlike Haskell and ML that support parametric polymorphism, Agda types can be parameterized not just by types but also by values. Defining types that have arbitrary values as parameters is what we call a dependent type.

The head function for vectors does not have to use Maybe or other tricks to deal with empty list. Since vectors carry their size in its type, we can just specify that the function should be applied just to non-empty vectors, i.e., values with type of the form Vec A (suc n). The code for this function is given below:

head : ∀ {A : Set}{n : ℕ} → Vec A (suc n) → A
head (x ∷ _) = x

Other function that we need to use tricks to implement it in Haskell, is zip, that combine two lists in a list of pairs. What should be returned when the lists does not have the same length? The Haskell library’s solution is to return a empty list when one of the parameters become empty.

zipList : ∀ {A B} → List A → List B → List (A × B)
zipList [] ys = []
zipList (x ∷ xs) [] = []
zipList (x ∷ xs) (y ∷ ys) = (x , y) ∷ zipList xs ys

Again, the problem is that list data type does not give us enough information about “garbage” values, so we are forced to use some trick like discard the remaining elements of the greater list.

With vectors, we avoid this situation by requiring that the vectors passed as arguments does have the same length. As a bonus, we have that the zip function type also guarantee that the result list does have the same size of the input lists.

zip : ∀ {A B n} → Vec A n → Vec B n → Vec (A × B) n
zip [] [] = []
zip (x ∷ xs) (y ∷ ys) = (x , y) ∷ zip xs ys

The reader must noticed that I said nothing about pairs. Next section will fix this little mistake.

A little digression: Dependent Products

Dependent products, or Σ-types, are a generalization of product types present in Haskell and ML in such a way that second component’s type depends on first component’s value.

Dependent products have the following definition in Agda:

  record Σ {l l'}(A : Set l)(B : A → Set l') : Set (l ⊔ l') where
    constructor _,_
    field
      fst : A
      snd : B fst

I have defined this type using record notation. Records allow us to define fields for some components of the type being defined. Also fields automatically generate record projection functions, as in Haskell. In the previous definition, the record \(\Sigma\) has the projection functions fst, that returns the first component of a dependent product, and snd that returns the second component.

Since Haskell (or ML) like products are a special case of dependent products, we can easily define one in terms of the other. Such definition is presented below:

_×_ : ∀ (A B : Set) → Set
A × B = Σ A (λ _ → B)

As an aside, each record declaration defines a module. So, we can open a record definition, like a module, in order to bring to the scope the projection functions and constructors defined in the record.

Finite set type

Finite sets are a \(\mathbb{N}\)-indexed type with \(n : \mathbb{N}\) elements:

data Fin : ℕ → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

You should noticed that:

• There’s no value of Fin 0, since all Fin’s constructors have indices of shape suc n, for some \(n : \mathbb{N}\).
• The type Fin n is inhabited by exactly \(n\) elements, i.e, the type Fin 2 has the following elements: zero : Fin 2 and suc zero : Fin 2. If v : Fin n then suc v has type Fin (suc n) and the effect of using Fin’s suc constructor is that we are increasing the finite set’s size by one.

Here I’ll not present the elimination principle for Fin because its type is long and it doesn’t render well to html. It’s defined in the Agda source code of this post on github.

Using finite sets to define a safe lookup function

Defining a function for looking up a element in a given position of a list is quite straightforward:

lookupList : ∀ {A} → ℕ → List A → Maybe A
lookupList _ [] = nothing
lookupList zero (x ∷ _) = just x
lookupList (suc n) (_ ∷ xs) = lookupList n xs

the problem here is that we are using Maybe type just to ensure that this function is total.

The use of Maybe is just to avoid the case that we pass an invalid index to lookupList function (invalid means that the index passed is greater than the list length). We can just rule out this using finite sets and vectors, since both are indexed by natural numbers, we can guarantee, using a type, that only valid indexes can be passed. Below is the code for the lookup function that uses finite sets and vectors:

lookup : ∀ {A : Set}{n} → Fin n → Vec A n → A
lookup zero (x ∷ xs) = x
lookup (suc n') (_ ∷ xs) = lookup n' xs

Since Vec A n is a type of vectors with n elements and Fin n is a type of n elements, using an index of type Fin n in a vector of type Vec A n simply rule out all invalid indexes! Cool!

Closing up

In this post I’ve presented examples of indexed data types - vectors and finite sets - and used them to define a safe lookup function. In the next posts we will continue our adventure through Agda programming language and its wonderful world of dependently typed programming.

See you on the next chapter of this series…