module Functions.Large where open import Data.Nat using (ℕ; zero; suc) open import Data.Empty using (⊥) open import Data.Unit using (⊤; tt) open import Data.Sum using (_⊎_; inj₁; inj₂)
Function definitions give another possibility to define sets. Here we will give general design guidelines on which language construct to use in certain situations.
_≤_Consider the inductive definition of _≤_ as follows:
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {m n : ℕ} → m ≤ n → suc m ≤ suc n
that will yield the following statements:
z≤n : 0 ≤ 0
z≤n : 0 ≤ 1
z≤n : 0 ≤ 2
...
s≤s z≤n : 1 ≤ 1
s≤s z≤n : 1 ≤ 2
s≤s z≤n : 1 ≤ 3
...
s≤s (s≤s z≤n) : 2 ≤ 2
s≤s (s≤s z≤n) : 2 ≤ 3
s≤s (s≤s z≤n) : 2 ≤ 4
..._≤_In comparison, now consider the recursive definition of _≤_ as follows (written as _≤′_):
_≤′_ : ℕ → ℕ → Set zero ≤′ n = ⊤ suc m ≤′ zero = ⊥ suc m ≤′ suc n = m ≤′ n
that will yield the following statements:
tt : 0 ≤′ 0
tt : 0 ≤′ 1
tt : 0 ≤′ 2
...
tt : 1 ≤′ 1
tt : 1 ≤′ 2
tt : 1 ≤′ 3
...
tt : 2 ≤′ 2
tt : 2 ≤′ 3
tt : 2 ≤′ 4
..._≤_ and _≤′_ have the same type and define exactly the same relations. But note that:
Inductive definitions are better than recursive definitions with pattern matching.
Suppose that we have n : ℕ, m : ℕ in a function definition.
In case of e : n ≤ m, we can pattern match on e -- the possible cases are z≤n and s≤s x.
In case of e : n ≤′ m, we cannot pattern match on e, because the type of e is not yet known to be either ⊥ or ⊤. We should pattern match on n and m before to we could learn more about n ≤′ m.
For example (we are going to discuss dependent functions like this one later):
f : {n m : ℕ} → n ≤ m → n ≤ suc m
f z≤n = z≤n
f (s≤s x) = s≤s (f x)
f′ : {n m : ℕ} → n ≤′ m → n ≤′ suc m
f′ {zero} {m} tt = tt
f′ {suc n} {zero} ()
f′ {suc n} {suc m} x = f′ {n} {m} x
Give recursive definitions for _≡_ and _≢_ on natural numbers.
Give mutual recursive definitions for the Even and Odd sets.
Set definitionsWe can create macro-like function definitions that do not pattern match on their argument:
_<_ : ℕ → ℕ → Set n < m = suc n ≤ m
Although we could have an inductive definition of _<_, this definition is better because no conversion functions are needed between _≤_ and _<_.
On the other hand, while the following would be also possible:
Maybe : Set → Set Maybe A = ⊤ ⊎ A
in general, this is not advised because then we cannot distinguish Maybe ⊤ from ⊤ ⊎ ⊤, for example.
We can summarize the general rule as follows:
Macro-like Set definitions are better than inductive definitions if we do not want to distinguish the new (derived) type from the base type.
Define _>_ and _≥_ on top of _≤_.
A good example of the macro-like behavior is the definition of the ¬ function. This is used to create a shorthand for writing negated statements (which we are also going to use later).
¬ : Set → Set ¬ A = A → ⊥
FinRecall the definition of the Fin indexed type from earlier:
data Fin : ℕ → Set where zero : (n : ℕ) → Fin (suc n) suc : (n : ℕ) → Fin n → Fin (suc n)
With this in mind, consider the Fin₀ function, where Fin₀ n is isomorphic to Fin n for all n:
Fin₀ : ℕ → Set Fin₀ zero = ⊥ Fin₀ (suc n) = ⊤ ⊎ Fin₀ n
Compare the produced elements:
n Fin₀ n Fin n
------------------------------------------------------------------
0 { } { }
1 { inj₁ tt } { zero }
2 { inj₁ tt { zero
, inj₂ (inj₁ tt) } , suc zero }
3 { inj₁ tt { zero
, inj₂ (inj₁ tt) , suc zero
, inj₂ (inj₂ (inj₁ tt) } , suc (suc zero) }
4 { inj₁ tt { zero
, inj₂ (inj₁ tt) , suc zero
, inj₂ (inj₂ (inj₁ tt)) , suc (suc zero)
, inj₂ (inj₂ (inj₂ (inj₁ tt))) } , suc (suc (suc zero)) }
...Based on the table above, we can observe the following pattern:
zero ~ inj₁ ttsuc ~ inj₂