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)

Definition

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.

Example

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)

Exercise

The ordering view is a view on ℕ × ℕ (in curried form):

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

Define the ordering view!

Individual constructors

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 * )
  odd  : ∀ n → Parity ( + n * )

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

Exercises

Define the functions

parity′ : ∀ n → Parity n

compare : ∀ m n → Ordering m n

Usage of views

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.

Exercises

1. Define division by 2 with the help of Parity:

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

2. Define congruence classes of 4 as a view on natural numbers!
   Hint: use Parity when implementing the view function.