# Exercise Sheet 1
This exercise sheet is based on the following lecture notes:
* https://git.cs.bham.ac.uk/drg/logic-and-computation-2019/tree/master/w08.1
* https://git.cs.bham.ac.uk/drg/logic-and-computation-2019/tree/master/w08.2
## Questions:
* Define the data type of _week-days_.
“`
data WeekDay : Set where
Monday Tuesday Wednesday Thursday Friday Saturday Sunday : WeekDay
“`
* Define the type construction of _triples_ (tuples with three components).
“`
data Triple (A B C : Set) : Set where
triple : A -> B -> C -> Triple A B C
“`
* Define a type of _sums_ with three components.
“`
data Sum3 (A B C : Set) : Set where
left : A -> Sum3 A B C
middle : B -> Sum3 A B C
right : C -> Sum3 A B C
“`
* Can we define any element of `Prod A Void` for some `A`? If not, why? If yes, give an example.
To construct an element of `Prod A Void`, we use the `pair` constructor, for which we need to find an element of `A` and an element of `Void`. However, `Void` has no constructors, so we cannot define any elements.
* Can we define any element of `Sum A Void` for some `A`? If not, why? If yes, give an example.
To construct an element of `Sum A Void`, we can either use the `left` constructor, for which we need an element of `A`, or the `right` constructor, for which we need an element of `Void`. While we do not have any constructors for `Void`, an element `a:A` is given by the question, so we may give `left a : Sum A Void`.
* Define directly (by pattern matching) the “negated or” operator `nor`. Also include the type.
“`
nor : Boolean -> Boolean -> Boolean
nor false false = true
nor _ _ = false
“`
* Define `Boolean` operators only using `nand`: `and`, `or`, `nor`, `imply`. Also include the type.
“`
and : Boolean -> Boolean -> Boolean
and x y = nand (nand x y) (nand x y)
or : Boolean -> Boolean -> Boolean
or x y = nand (nand x x) (nand y y)
nor : Boolean -> Boolean -> Boolean
nor x y = nand orxy orxy where
orxy : Boolean
orxy = nand (nand x x) (nand y y)
imply : Boolean -> Boolean -> Boolean
imply x y = nand x (nand y y)
“`
* Write a function `swap` which given an element of `Prod A B` creates another product using the same components but in the other order. Also include the type. Provide two solutions:
* direct definition, using pattern matching
“`
swap : {A B : Set} -> Prod A B -> Prod B A
swap (pair a b) = pair b a
“`
* indirect definition, not using pattern matching but using the projections.
“`
swap : {A B : Set} -> Prod A B -> Prod B A
swap z = pair (proj2 z) (proj1 z)
“`
* Write an `and : Prod Boolean Boolean -> Boolean` function.
“`
and : Prod Boolean Boolean -> Boolean
and (pair true true) = true
and _ = false
“`
* Construct conversion functions between the following types. Also include the type.
* `Prod Unit A` and `A`
“`
to : {A : Set} -> Prod Unit A -> A
to (pair _ a) = a
from : {A : Set} -> A -> Prod Unit A
from a = pair empty a
“`
* `Sum A B` and `Sum B A`
“`
to : {A B : Set} -> Sum A B -> Sum B A
to (left a) = right a
to (right b) = left b
from : {A B : Set} -> Sum B A -> Sum A B
from (left b) = right b
from (right a) = left a
“`
* `Prod A (Sum B C)` and `Sum (Prod A B) (Prod A C)`
“`
to : {A B C : Set} -> Prod A (Sum B C) -> Sum (Prod A B) (Prod A C)
to (pair a (left b)) = left (pair a b)
to (pair a (right c)) = right (pair a c)
from : {A B C : Set} -> Sum (Prod A B) (Prod A C) -> Prod A (Sum B C)
from (left (pair a b)) = pair (left b)
from (right (pair a c)) = pair (right c)
“`
* `A` and `Sum A Void`, `Sum Void A`
“`
to1 : {A : Set} -> A -> Sum A Void
to1 a = left a
to2 : {A : Set} -> A -> Sum Void A
to2 a = right a
from1 : {A : Set} -> Sum A Void -> A
from1 (left a) = a
from2 : {A : Set} -> Sum Void A -> A
from2 (right a) = a
“`
* `Prod A Void` and `Void`
“`
to : {A : Set} -> Prod A Void -> Void
to (pair _ v) = v
from : {A : Set} -> Void -> Prod A Void
from ()
“`