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

_++_ : Concatenation on Lists

Definition of concatenation:


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

infixr 5 _++_

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


fromList : List   


toList   :   List 

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 4 _,_
infixr 2 _×_

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 1 _⊎_

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)