module Functions.Views where open import Data.Nat using (ℕ; zero; suc; _<_; _>_; s≤s; z≤n; _+_; _*_) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Relation.Binary.PropositionalEquality using (_≡_; refl)

Let `A`

be a type.

Let `P : A → Set`

a disjunction (parameterized on `A`

).

A *view on A* is a function with type

`(a : A) → P a`

.Assume the following definitions.

data Even : ℕ → Set data Odd : ℕ → Set data Even where zero : Even zero odd : ∀ {n} → Odd n → Even (suc n) data Odd where even : ∀ {n} → Even n → Odd (suc n)

The parity view:

parity : ∀ n → Even n ⊎ Odd n parity zero = inj₁ zero parity (suc n) with parity n parity (suc n) | inj₁ x = inj₂ (even x) parity (suc n) | inj₂ y = inj₁ (odd y)

The ordering view is a view on `ℕ × ℕ`

(in curried form):

ordering : ∀ n m → n < m ⊎ n ≡ m ⊎ n > m

Define the ordering view!

The disjunction of the view can be replaced by an individual data type:

`Even n ⊎ Odd n`

~ `Parity n`

where

data Parity : ℕ → Set where even : ∀ n → Parity (n * 2) odd : ∀ n → Parity (1 + n * 2)

`n < m ⊎ n ≡ m ⊎ n > m`

~ `Ordering n m`

where

data Ordering : ℕ → ℕ → Set where less : ∀ m k → Ordering m (suc (m + k)) equal : ∀ m → Ordering m m greater : ∀ m k → Ordering (suc (m + k)) m

Define the functions

parity′ : ∀ n → Parity n

compare : ∀ m n → Ordering m n

If we pattern match on `parity n`

we learn not only whether `n`

is even or odd but we also get a proof of it. From the proof we can get additional information too (like what is the half of `n`

).

Views are very handy with the `with`

construct.

- Define division by 2 with the help of
`Parity`

:

⌊_/2⌋ : ℕ → ℕ -- half (⌊ 1 /2⌋ = 0)

- Define congruence classes of 4 as a view on natural numbers!

Hint: use`Parity`

when implementing the view function.