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