# Types Summer School 2007

The Types Summer School 2007 is held in Bertinoro, Italy, August 19 - 31.

The examples from the lectures can be found here: examples/SummerSchool07/Lecture

## Exercises

### 1. Natural numbers

1.1. Define a datatype of `Nat`

natural numbers with constructors `zero`

and `suc`

.

1.2. Define an addition function `_+_`

on natural numbers, by recursion over the first argument.

1.3. Define multiplication.

1.4. Given the identity type

data _==_ {A : Set}(x : A) : A → Set where refl : x == x

prove that _+_ is associative, i.e. give a function

assoc : (x y z : Nat) → (x + (y + z)) == ((x + y) + z)

### 2. Vectors

Vectors are lists of a fixed length:

data Vec (A : Set) : Nat → Set where ε : Vec A zero _►_ : {n : Nat} → A → Vec A n → Vec A (suc n)

2.1. Define a function `vec`

which computes a vector where all the elements are the same.

vec : {A : Set}{n : Nat} → A → Vec A n

Hint: you need to do recursion over n

2.2. Define a function `_<*>_`

to point-wise apply a vector of functions to a vector of arguments.

_<*>_ : {A B : Set}{n : Nat} → Vec (A → B) n → Vec A n → Vec B n

2.3. Use `vec`

and `_<*>_`

to define a function

map : {A B : Set}{n : Nat} → (A → B) → Vec A n → Vec B n

2.4. Use `vec`

and `_<*>_`

to define a function

zip : {A B C : Set}{n : Nat} → (A → B → C) → Vec A n → Vec B n → Vec C n

### 3. Finite sets

The family of finite sets indexed by size is defined by:

data Fin : Nat → Set where fzero : {n : Nat} → Fin (suc n) fsuc : {n : Nat} → Fin n → Fin (suc n)

The elements of `Fin n`

are the natural numbers less than `n`

(but with different names for the constructors).

3.1. Show that there are no elements in `Fin zero`

, i.e. give a function

empty : Fin zero → False

where

data False : Set where

is the empty datatype. Hint: use an absurd pattern `()`

.

3.2. We can use elements of finite sets as positions in vectors. Define a look up function

_!_ : {A : Set}{n : Nat} → Vec A n → Fin n → A

3.3. In fact, `_!_`

is an isomorphism between `Vec A n`

and `Fin n → A`

. Define its inverse

tabulate : {A : Set}{n : Nat} → (Fin n → A) → Vec A n

### 4. Predicates over lists

The list datatype is given by

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

4.1. Define `map`

and `_++_`

for lists.

map : {A B : Set} → (A → B) → List A → List B _++_ : {A : Set} → List A → List A → List A

4.2. Define a datatype family `All P`

which represents proofs that `P`

holds for all elements of a list

data All {A : Set}(P : A → Set) : List A → Set where

4.3. Define a datatype family `Some P`

which represents proofs that `P`

holds for some element of a list

data Some {A : Set}(P : A → Set) : List A → Set where

4.4. State and prove some interesting lemmas about the interaction between `All`

and `Some`

and the list functions `map`

and `_++_`

.

4.5. Define list membership in terms of `Some`

.

_∈_ : {A : Set} → A → List A → Set

Hint: you need to use the identity type from exercise 1.4.

4.6. We can define natural numbers as lists:

record True : Set where tt : True tt = record {} — the unique element of True Nat = List True zero : Nat zero = [] suc : Nat → Nat suc n = tt :: n

Now define `Vec`

and `Fin`

using `All`

and `Some`

.

4.7. Dependent pairs can be defined by

data _×_ (A : Set)(B : A → Set) : Set where _,_ : (x : A) → B x → A × B

We can recover the simply typed pairs:

_∧_ : (A B : Set) → Set A ∧ B = A × \_ → B

Now if you know `All P xs`

and `Some Q xs`

then you can get an `A`

satisfying both `P`

and `Q`

. Prove this by defining the following look up function:

_!_ : {A : Set}{P : A → Set}{Q : A → Set}{xs : List A} → All P xs → Some Q xs → A × (\z → P z ∧ Q z)

4.8. (*Harder*) For a decidable predicate it is the case that it either holds for each element in a list, or there is an element for which it doesn’t hold. Given

¬_ : Set → Set ¬ P = P → False data _∨_ (A B : Set) : Set where inl : A → A ∨ B inr : B → A ∨ B data Bool : Set where false : Bool true : Bool data IsTrue : Bool → Set where isTrue : IsTrue true Holds : {A : Set} → (A → Bool) → A → Set Holds p x = IsTrue (p x)

define the function `all`

:

all : {A : Set}(p : A → Bool)(xs : List A) → All (Holds p) xs ∨ Some (\x → ¬ Holds p x) xs

Hint: you might find the function `decide`

helpful

decide : {A : Set}(p : A → Bool)(x : A) → Holds p x ∨ ¬ Holds p x