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