# TypesSummerSchool2007

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
```