quox/examples/maybe.quox

68 lines
1.8 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

load "misc.quox"
load "either.quox"
namespace maybe {
def0 Tag : ★ = {nothing, just}
def0 Payload : Tag → ★ → ★ =
λ tag A ⇒ case tag return ★ of { 'nothing ⇒ True; 'just ⇒ A }
def0 Maybe : ★ → ★ =
λ A ⇒ (t : Tag) × Payload t A
def tag : 0.(A : ★) → ω.(Maybe A) → Tag =
λ _ x ⇒ caseω x return Tag of { (tag, _) ⇒ tag }
def Nothing : 0.(A : ★) → Maybe A =
λ _ ⇒ ('nothing, 'true)
def Just : 0.(A : ★) → A → Maybe A =
λ _ x ⇒ ('just, x)
def0 IsJustTag : Tag → ★ =
λ t ⇒ case t return ★ of { 'just ⇒ True; 'nothing ⇒ False }
def0 IsJust : (A : ★) → Maybe A → ★ =
λ A x ⇒ IsJustTag (tag A x)
def is-just? : 0.(A : ★) → ω.(x : Maybe A) → Dec (IsJust A x) =
λ A x ⇒
caseω tag A x return t ⇒ Dec (IsJustTag t) of {
'just ⇒ Yes True 'true;
'nothing ⇒ No False (λ x ⇒ x)
}
def0 nothing-unique :
(A : ★) → (x : True) → ('nothing, x) ≡ Nothing A : Maybe A =
λ A x ⇒
case x return x' ⇒ ('nothing, x') ≡ Nothing A : Maybe A of {
'true ⇒ δ _ ⇒ ('nothing, 'true)
}
def elim :
0.(A : ★) →
0.(P : Maybe A → ★) →
ω.(P (Nothing A)) →
ω.((x : A) → P (Just A x)) →
(x : Maybe A) → P x =
λ A P n j x ⇒
case x return x' ⇒ P x' of { (tag, payload) ⇒
(case tag
return t ⇒
0.(eq : tag ≡ t : Tag) → P (t, coe (i ⇒ Payload (eq @i) A) payload)
of {
'nothing ⇒
λ eq ⇒
case coe (i ⇒ Payload (eq @i) A) payload
return p ⇒ P ('nothing, p)
of { 'true ⇒ n };
'just ⇒ λ eq ⇒ j (coe (i ⇒ Payload (eq @i) A) payload)
}) (δ _ ⇒ tag)
}
}
def0 Maybe = maybe.Maybe
def0 Just = maybe.Just
def0 Nothing = maybe.Nothing