module Sets.Parametric where open import Data.Nat

`List`

Definition of `List`

:

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

*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 ∷ []
...
```

- What is the connection between
`List ⊤`

and`ℕ`

? - Define a
`Maybe`

set (lists with 0 or 1 elements). - Define parametric trees (various sorts).

`_×_`

: Cartesian productDefinition of Cartesian product:

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

`(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
```

- How many elements are there in
`⊤ × ⊤`

,`⊤ × ⊥`

,`⊥ × ⊤`

and`⊥ × ⊥`

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

- What are the elements of
`Bool ⊎ ⊤`

? - What are the elements of
`⊤ ⊎ (⊤ ⊎ ⊤)`

? - Name a type isomorphic to
`⊤ ⊎ ⊤`

that you have already seen before. - How should we define
`Bottom`

so that ∀ A : Set .`Bottom ⊎ A`

would be isomorphic to`A`

(i.e. neutral element of`_⊎_`

)? - Give an isomorphic definition of
`Maybe A`

with the help of`_⊎_`

and`⊤`

.

`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

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

!

Consider the following data set:

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

List the 4 smallest elements of `AlterList ⊤ Bool`

, and the 5 smallest elements of `AlterList Bool ⊤`

.

`Square`

, the set of square matrices with 2^{n} 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:*

Set | 1st, | 2nd, | 3rd, | ... |
---|---|---|---|---|

`Square ℕ` = { |
`zero 3` ; `zero 16` ; ...; |
`suc (zero (t4 1 2 3 4))` ; ...; |
`x` ;...; |
... |

`Square (T4 ℕ)` = { |
`zero (t4 1 2 3 4)` ; ...; |
`suc (zero (t4 (t4 ...) ...))` ; ...; |
...; | ... |

`Square (T4 (T4 ℕ))` = { |
`zero (t4 (t4 ...) ...)` ; ...; |
...; | ...; | ... |

... | ... | ... | ... | ... |

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