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 _∷_
_++_
: Concatenation on ListsDefinition of concatenation:
_++_ : {A : Set} → List A → List A → List A [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys) infixr 5 _++_
_++_
works with List
s parametrised by arbitrary Set
s. 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.
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
.
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
functionid : {A : Set} → A → A id a = a
If we want, can specify the implicit parameter manually in curly braces:
aNumber = id {ℕ} (suc zero)
Define const : {A B : Set} → A → B → A
!
Define flip : {A B C : Set} → (A → B → C) → B → A → C
!
_×_
: Cartesian ProductRecall the definition of Cartesian product:
data _×_ (A B : Set) : Set where _,_ : A → B → A × B infixr 4 _,_ infixr 2 _×_
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 1 _⊎_
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)