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  _∷_

_++_ : Concatenation on Lists

Definition of concatenation:

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

infixr  _++_

_++_ works with Lists parametrised by arbitrary Sets. We call this parameter a polymorphic parameter and _++_ 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.

Exercises

• Define two functions which define the isomorphism between List ⊤ and ℕ!

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

• Define a Maybe set (lists with 0 or 1 elements) and head and tail functions for the polymorphic List type with the help of Maybe.

Exercises

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

Polymorphic id function

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

If we want, can specify the implicit parameter manually in curly braces:

aNumber = id {ℕ} (suc zero)

Exercise

Define const : {A B : Set} → A → B → A!

Define flip : {A B C : Set} → (A → B → C) → B → A → C!

_×_: Cartesian Product

Recall the definition of Cartesian product:

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

infixr  _,_
infixr  _×_

Exercises

Define a function which swaps the two elements!

Define the following functions:

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

_⊎_: Disjoint Union (Sum)

Recall the definition

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

infixr  _⊎_

Exercises

Define a function which swaps the two elements!

Define the eliminator function for disjoint union:

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