Indexed Data Types

The source code for this module: PartI/Indexed.ard
The source code for the exercises: PartI/IndexedEx.ard

In this module we illustrate the concepts that we discussed in the previous modules through a bunch of examples of definitions and proofs.

We define the function sort that sorts lists by insertion sort and the function reverse that reverses them.

We discuss two more examples of proofs: we prove that reverse is an involution and that + : Nat -> Nat -> Nat is associative.

Next, we turn to a several examples of data types. For a given type A, we exhibit two possible definitions of the type of fixed length vectors of elements of A, one of which is based on data types with constructor patterns. We conclude with a discussion of possible definitions of the type of all finite sets.

Insertion sort and reverse

Among the sorting algorithms, perhaps, the simplest to define in a dependently typed language is the insertion sort. The kind of recursion used in the insertion sort parallels the inductive definition of the type List.

If our list is nil, then we have nothing to do and simply return nil. Otherwise, if the list is of the form cons x xs, invoke sort recursively on xs and insert x into the result using the function insert, in turn defined by recursion on List:

\func if {A : \Type} (b : Bool) (t e : A) : A \elim b
  | true => t
  | false => e

\func sort {A : \Type} (less : A -> A -> Bool) (xs : List A) : List A \elim xs
  | nil => nil
  | cons x xs => insert less x (sort less xs)
  \where
    \func insert {A : \Type} (less : A -> A -> Bool) (x : A) (xs : List A) : List A \elim xs
      | nil => cons x nil
      | cons x' xs => if (less x x') (cons x (cons x' xs)) (cons x' (insert less x xs))

In case the predicate less defines a linear order, the result of the function sort is a sorted permutation of its argument xs. This specification of correctness of sort can be phrased in Arend as follows:

\func isLinOrder {A : \Type} (lessOrEq : A -> A -> Bool) : \Type => {?}
\func isSorted {A : \Type} (lessOrEq : A -> A -> Bool) (xs : List A) : \Type => {?}
-- isPerm says that xs' is permutation of xs
\func isPerm {A : \Type} (xs xs' : List A) : \Type => {?}
\func sort-isCorrect {A : \Type} (lessOrEq : A -> A -> Bool) (p : isLinOrder lessOrEq) (xs : List A)
       : \Sigma (isSorted lessOrEq (sort lessOrEq xs)) (isPerm xs (sort lessOrEq xs)) => {?}

It is possible to write definitions of the predicates and a proof for sort-isCorrect with the arsenal of language constructs that we have introduced by now. However, as we will see in the subsequent modules, there are better ways to do this, and for that reason we omit the details here. A proper proof will be given later.

Consider another, simpler, operation on lists: reversion. We define the function reverse that reverses a list xs via an auxiliary function that accumulates reversed sublists in the extra parameter acc:

\func reverse {A : \Type} (xs : List A) : List A => rev nil xs
  \where
    \func rev {A : \Type} (acc xs : List A) : List A \elim xs
      | nil => acc
      | cons x xs => rev (cons x acc) xs

-- reverse (cons x xs) => rev nil (cons x xs) => rev (cons x nil) xs
-- reverse (reverse (cons x xs)) => reverse (rev (cons x nil) xs) => rev nil (rev (cons x nil) xs)

Below we prove that reverse is an involution.

Examples of proofs: +-assoc and reverse-isInvolution

If you try to prove reverse (reverse xs) = xs directly by induction, then you will stuck at proving the equality rev nil (rev (cons x nil) xs) = cons x xs, because induction hypothesis is too weak. The statement should be strengthened in order to make induction hypothesis stronger. Namely, we should prove a more general property of reverse.rev and conclude that reverse is involution as a consequence:

\func reverse-isInvolutive {A : \Type} (xs : List A) : reverse (reverse xs) = xs => rev-isInv nil xs
  \where
    \func rev-isInv {A : \Type} (acc xs : List A) : reverse (reverse.rev acc xs) = reverse.rev xs acc \elim xs
      | nil => idp
      | cons x xs => rev-isInv (cons x acc) xs

For the proof of associativity of + we need the following property of = (congruence): if f : A -> B, x, y : A and there is a proof p : x = y, then there is a proof pmap f p : f x = f y. The proof of (x + y) + z = x + (y + z) is, of course, by induction, but one should carefully choose the parameter for induction. In our case, because we defined + by recursion on the right argument, we should choose z:

\func +-assoc (x y z : Nat) : (x + y) + z = x + (y + z) \elim z
  | 0 => idp
  | suc z => pmap suc (+-assoc x y z)
-- we can apply pmap because of the reductions:
-- (x + y) + suc z => suc ((x + y) + z)
-- x + (y + suc z) => x + suc (y + z) => suc (x + (y + z))

Lists of fixed length

Suppose we want to implement a function that takes a list and a natural number and returns the element in the list at the given index. It is impossible to do this in general since the index may be greater than the length of the list. One way to fix this problem is to pass a proof that the index is less than the length of the list:

Exercise 1: Implement the function lookup, which takes a list xs and a natural number n and returns the n-th element in the list. The function should also take a proof that n is in the right range: T (n < length xs).

There is another way to fix this problem. We could use a type of vectors, that is of lists, whose length is fixed and parameterized by n : Nat. One way to do this is by writing recursive function with codomain \Type:

\func vec (A : \Type) (n : Nat) : \Type \elim n
  | 0 => \Sigma
  | suc n => \Sigma A (vec A n)

\func head {A : \Type} (n : Nat) (xs : vec A (suc n)) => xs.1

\func tail {A : \Type} (n : Nat) (xs : vec A (suc n)) => xs.2

Alternatively, we can implement this type as a data type. It is a bit tricky since the data type Vec (A : \Type) (n : Nat) has constructor fcons A (Vec A m) if n is suc m and constructor fnil if n is 0. Such data types can be defined using constructors with patterns:

\data Vec (A : \Type) (n : Nat) \elim n
  | 0 => fnil
  | suc n => fcons A (Vec A n)

\func Head {A : \Type} {n : Nat} (xs : Vec A (suc n)) : A \elim xs
  | fcons x _ => x

\func Tail {A : \Type} {n : Nat} (xs : Vec A (suc n)) : Vec A n \elim xs
  | fcons _ xs => xs

There are several reasons, why the latter definition with data types is preferable. Firstly, Vec has named constructors, so we explicitly see which constructor we are dealing with. Secondly, in pattern matching we can use names for parameters of constructors instead of mere projections .1, .2, etc. These things make definitions like Vec much more convenient to work with than vec.

Below we use double recursion on n and xs to define the function first that returns the first element of a vector and the function append that appends a vector to other vector. Note that the output of first is not defined for the empty vector. This is typically resolved by using Maybe data type as codomain:

\data Maybe (A : \Type) | nothing | just A

\func first {A : \Type} {n : Nat} (xs : Vec A n) : Maybe A \elim n, xs
  | 0, fnil => nothing
  | suc n, fcons x xs => just x

\func append {A : \Type} {n m : Nat} (xs : Vec A n) (ys : Vec A m) : Vec A (m + n) \elim n, xs
  | 0, fnil => ys
  | suc _ , fcons x xs => fcons x (append xs ys)

Exercise 2: Implement function replicate for ‘vec’ and ‘Vec’ (this function creates the list of a given length filled with a given element).

Exercise 3: Implement function ‘map’ for ‘vec’ and ‘Vec’.

Exercise 4: Implement function ‘zipWith’ for ‘vec’ and ‘Vec’. The function must take lists of equal lengths.

Implicit arguments in Arend make possible to define rather useless function that computes the length of a vector:

\func length {A : \Type} {n : Nat} (xs : Vec A n) => n

Finite sets, lookup

There are several variants of definition of a type of finite sets as well. For example, one can define it as a subtype of Nat:

\func fin (n : Nat) => \Sigma (x : Nat) (T (x < n))

Or as a recursive function:

\func Fin' (n : Nat) : \Set0
  | 0 => Empty
  | suc n => Maybe (Fin' n)

Or as a data type:

\data Fin (n : Nat) \with
  | suc n => { fzero | fsuc (Fin n) }

Consider several examples:

-- Fin 0 -- empty type
\func absurd {A : \Type} (x : Fin 0) : A

\func fin0 : Fin 3 => fzero
\func fin1 : Fin 3 => fsuc fzero
\func fin2 : Fin 3 => fsuc (fsuc fzero)
-- The following does not typecheck
-- \func fin3 : Fin 3 => fsuc (fsuc (fsuc fzero))

It can be easily proven that Fin 3 has no more than three elements. Specifically, it can be proven that every element of Fin 3 is either fin0, fin1 or fin2:

\func atMost3 (x : Fin 3) : Either (x = fin0) (Either (x = fin1) (x = fin2)) \elim x
  | fzero => inl idp
  | fsuc fzero => inr (inl idp)
  | fsuc (fsuc fzero) => inr (inr idp)
  | fsuc (fsuc (fsuc ()))

The embedding to Nat can be defined as follows:

\func toNat {n : Nat} (x : Fin n) : Nat
  | {suc _}, fzero => 0
  | {suc _}, fsuc x => suc (toNat x)

The type Fin n can be particularly useful, for example, in a definition of a safe lookup in a vector:

\func lookup {A : \Type} {n : Nat} (xs : Vec A n) (i : Fin n) : A \elim n, xs, i
  | suc _, fcons x _, fzero => x
  | suc _, fcons _ xs, fsuc i => lookup xs i

Exercise 5: Functions Fin n -> A correspond to lists of length n with elements in A. Implement the function that converts an element of Fin n -> A to element of Vec A n.

Exercise 6: Define the type of matrices and a number of functions for them: the diagonal matrix, transpose, addition and multiplication of matrices.

Exercise 7: Define the type CTree A n of (complete and full) binary trees of height precisely n, which store elements in internal nodes, but not in leaves. The height of a leaf is 0.

Exercise 8: Define the type Tree A n of binary trees of height at most n, which store elements in internal nodes, but not in leaves. The height of a leaf is 0. Define the function that computes the height of a tree.