Import list

module Sets.Parametric where
open import Data.Nat

Definition of List

Definition of List:

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

infixr  _∷_

Interpretation: List A ∈ Set, where A ∈ Set. We call A a parameter of List and we can refer to A in the definition of the set elements.

Example: Note that the elements of List Bool are as follows:

[]  
true  ∷ []  
false ∷ []
true  ∷ true  ∷ []  
false ∷ true  ∷ []  
true  ∷ false ∷ []  
false ∷ false ∷ []  
...

Exercises

1. What is the connection between List ⊤ and ℕ?
2. Define a Maybe set (lists with 0 or 1 elements).
3. Define parametric trees (various sorts).

_×_: Cartesian product

Definition of Cartesian product:

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

infixr  _,_
infixr  _×_

(A B : Set) is the way of specifying a set that is parameterized by two (other) sets.

Example: Elements of Bool × Bool (the extra space is needed before the comma):

 true , true
 true , false
 false , true
 false , false

Exercises

1. How many elements are there in ⊤ × ⊤, ⊤ × ⊥, ⊥ × ⊤ and ⊥ × ⊥?
2. How should we define Top so that ∀ A : Set .Top × A would be isomorphic to A (i.e. neutral element of _×_)?

_⊎_: Disjoint union (sum)

Definition:

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

infixr  _⊎_

Exercises

1. What are the elements of Bool ⊎ ⊤?
2. What are the elements of ⊤ ⊎ (⊤ ⊎ ⊤)?
3. Name a type isomorphic to ⊤ ⊎ ⊤ that you have already seen before.
4. How should we define Bottom so that ∀ A : Set . Bottom ⊎ A would be isomorphic to A (i.e. neutral element of _⊎_)?
5. Give an isomorphic definition of Maybe A with the help of _⊎_ and ⊤.

Mutually recursive sets

List₁ and List₂ are mutually recursive parametric sets:

data List₁ (A B : Set) : Set
data List₂ (A B : Set) : Set

data List₁ (A B : Set) where
  []  :                 List₁ A B
  _∷_ : A → List₂ A B → List₁ A B

data List₂ (A B : Set) where
  _∷_ : B → List₁ A B → List₂ A B

Exercise

List the smallest first 7 elements of List₁ ⊤ Bool!

Non-regular recursive set

Consider the following data set:

data AlterList (A B : Set) : Set  where
  []  :                     AlterList A B
  _∷_ : A → AlterList B A → AlterList A B

Exercise

List the 4 smallest elements of AlterList ⊤ Bool, and the 5 smallest elements of AlterList Bool ⊤.

Nested set

Square, the set of square matrices with 2ⁿ rows, is nested, because at least one of its constructors refers to the set defined with more complex parameters:

data T4 (A : Set) : Set where
  t4 : A → A → A → A → T4 A

data Square (A : Set) : Set where
  zero :            A  → Square A   -- 2^0 rows
  suc  : Square (T4 A) → Square A   -- 2^(n + 1) rows

Example:

x : Square ℕ
x = suc (suc (zero (t4 (t4 1 2 3 4) (t4 5 6 7 8) (t4 9 10 11 12) (t4 13 14 15 16))))

$\left(\begin{array}{cccc}\hfill 1\hfill & \hfill 2\hfill & \hfill 5\hfill & \hfill 6\hfill \\ \hfill 3\hfill & \hfill 4\hfill & \hfill 7\hfill & \hfill 8\hfill \\ \hfill 9\hfill & \hfill 10\hfill & \hfill 13\hfill & \hfill 14\hfill \\ \hfill 11\hfill & \hfill 12\hfill & \hfill 15\hfill & \hfill 16\hfill \end{array}\right)$

Nested sets are special non-regular sets. Nested sets can be translated to mutually recursive regular sets.