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)