# Import list


module Functions.Polymorphic where

open import Data.Nat
open import Data.Unit using (⊤; tt)

# Definition of 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 lists

Using 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 Lists parametrised by arbitrary Sets. 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.

## Exercises

1. Define two functions that define an isomorphism between List ⊤ and ℕ. That is, the following functions should be implemented:

fromList : List ⊤ → ℕ
toList : ℕ → List ⊤

2. 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).

3. 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.

4. 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

5. Define the singleton list function:

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

# Polymorphic identity function: 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)

## Exercises

1. Define the const : {A B : Set} → A → B → A function.

2. Define the flip : {A B C : Set} → (A → B → C) → B → A → C function.

# _×_: Cartesian product

Recall the definition of the product set:


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

infixr 4 _,_
infixr 2 _×_

## Exercises

1. Define a function that swaps the two elements.

2. 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 _⊎_

## Exercises

1. Define a function that swaps the two elements.

2. Define the eliminator function for disjoint union:

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