module Functions.Polymorphic where open import Data.Nat open import Data.Unit using (⊤; tt)

`List`

Recall the definition of `List`

:

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

Remember this is a polymorphic definition.

`_++_`

: Concatenation on listsUsing the definition of the `List`

set above, the definition of list concatenation can be given as follows:

_++_ : {A : Set} → List A → List A → List A [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys) infixr 5 _++_

The `_++_`

operator works with `List`

s parametrised by arbitrary `Set`

s. We call its parameters polymorphic, and thus `_++_`

a polymorphic function. Polymorphic parameters have to be named explicitly in beginning of the declaration of the function by putting them into curly braces:

`f : {A B C : Set} → ...`

In Agda, polymorphic parameters are explicit, in Haskell they are implicit.

Instead of curly braces we can use also round braces but then we have to give the set as a parameter at every function call, which may make it clearer but also more inconvenient to use.

Define two functions that define an isomorphism between

`List ⊤`

and`ℕ`

. That is, the following functions should be implemented:`fromList : List ⊤ → ℕ`

`toList : ℕ → List ⊤`

Show on a sheet of paper with equational reasoning that the

`fromList`

function is a bijection and it preserves the`_+_`

and`_++_`

operations (that is,`∀ a, b ∈ List ⊤ . fromList (a ++ b) = fromList a + fromList b`

always holds).Define a

`Maybe`

set (a list with 0 or 1 elements) together with the`head`

and`tail`

functions for the polymorphic`List`

type, with the help of`Maybe`

.Define the following functions on lists:

`map : {A B : Set} → (A → B) → List A → List B -- regular map`

`maps : {A B : Set} → List (A → B) → List A → List B -- pairwise map`

Define the singleton list function:

`[_] : {A : Set} → A → List A`

`id`

Similarly to the concatenation function above, a polymorphic identity function can be also given with the same notation, which is an example of generic polymorphic functions.

id : {A : Set} → A → A id a = a

If we want we can specify the implicit (hidden) parameter manually in curly braces:

aNumber = id {ℕ} (suc zero)

Define the

`const : {A B : Set} → A → B → A`

function.Define the

`flip : {A B C : Set} → (A → B → C) → B → A → C`

function.

`_×_`

: Cartesian productRecall the definition of the product set:

data _×_ (A B : Set) : Set where _,_ : A → B → A × B infixr 4 _,_ infixr 2 _×_

Define a function that swaps the two elements.

Define the following functions:

`proj₁ : {A B : Set} → A × B → A`

`proj₂ : {A B : Set} → A × B → B`

`_⊎_`

: Disjoint union (sum)Recall the definition of the sum set:

data _⊎_ (A B : Set) : Set where inj₁ : A → A ⊎ B inj₂ : B → A ⊎ B infixr 1 _⊎_

Define a function that swaps the two elements.

Define the eliminator function for disjoint union:

`[_,_] : {A B C : Set} → (A → C) → (B → C) → (A ⊎ B → C)`