From 3c0989dcb237d9149022e13a5ced85b503eabad3 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 17 Jul 2023 03:52:12 +0200
Subject: [PATCH] maybe.quox

---
 examples/all.quox   |  1 +
 examples/maybe.quox | 68 +++++++++++++++++++++++++++++++++++++++++++++
 examples/misc.quox  | 22 +++++++--------
 3 files changed, 80 insertions(+), 11 deletions(-)
 create mode 100644 examples/maybe.quox

diff --git a/examples/all.quox b/examples/all.quox
index 2ccb163..b24ebcf 100644
--- a/examples/all.quox
+++ b/examples/all.quox
@@ -1,6 +1,7 @@
 load "misc.quox"
 load "bool.quox"
 load "either.quox"
+load "maybe.quox"
 load "nat.quox"
 load "pair.quox"
 load "list.quox"
diff --git a/examples/maybe.quox b/examples/maybe.quox
new file mode 100644
index 0000000..5c9878d
--- /dev/null
+++ b/examples/maybe.quox
@@ -0,0 +1,68 @@
+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 : ★) → 1.A → Maybe A =
+  λ _ x ⇒ ('just, x)
+
+def0 IsJustTag : ω.Tag → ★ =
+  λ t ⇒ caseω t return ★ of { 'just ⇒ True; 'nothing ⇒ False }
+
+def0 IsJust : 0.(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 :
+    0.(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 : 0.(Maybe A) → ★) →
+    ω.(P (Nothing A)) →
+    ω.(1.(x : A) → P (Just A x)) →
+    1.(x : Maybe A) → P x =
+  λ A P n j x ⇒
+  case1 x return x' ⇒ P x' of { (tag, payload) ⇒
+    (case1 tag
+     return t ⇒
+       0.(eq : tag ≡ t : Tag) → P (t, coe (i ⇒ Payload (eq @i) A) payload)
+     of {
+       'nothing ⇒
+          λ eq ⇒
+          case1 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
diff --git a/examples/misc.quox b/examples/misc.quox
index 8c6a8c1..ddc6414 100644
--- a/examples/misc.quox
+++ b/examples/misc.quox
@@ -1,36 +1,36 @@
-def0 True : ★ = {true};
+def0 True : ★ = {true}
 
-def0 False : ★ = {};
-def0 Not : 0.★ → ★ = λ A ⇒ ω.A → False;
+def0 False : ★ = {}
+def0 Not : 0.★ → ★ = λ A ⇒ ω.A → False
 
 def void : 0.(A : ★) → 0.False → A =
-  λ A v ⇒ case0 v return A of { };
+  λ A v ⇒ case0 v return A of { }
 
-def0 Pred : 0.★ → ★¹ = λ A ⇒ 0.A → ★;
+def0 Pred : 0.★ → ★¹ = λ A ⇒ 0.A → ★
 
 def0 All : 0.(A : ★) → 0.(Pred A) → ★¹ =
-  λ A P ⇒ 1.(x : A) → P x;
+  λ A P ⇒ 1.(x : A) → P x
 
 def cong :
     0.(A : ★) → 0.(P : Pred A) → 1.(p : All A P) →
     0.(x y : A) → 1.(xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) =
-  λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖);
+  λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖)
 
 def0 eq-f :
     0.(A : ★) → 0.(P : Pred A) →
     0.(p : All A P) → 0.(q : All A P) →
     0.A → ★ =
-  λ A P p q x ⇒ p x ≡ q x : P x;
+  λ A P p q x ⇒ p x ≡ q x : P x
 
 def funext :
     0.(A : ★) → 0.(P : Pred A) → 0.(p q : All A P) →
     1.(All A (eq-f A P p q)) → p ≡ q : All A P =
-  λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖;
+  λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖
 
 def sym : 0.(A : ★) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A =
-  λ A x y eq ⇒ δ 𝑖 ⇒ comp A (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 };
+  λ A x y eq ⇒ δ 𝑖 ⇒ comp A (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 }
 
 def trans : 0.(A : ★) → 0.(x y z : A) →
             ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A =
   λ A x y z eq1 eq2 ⇒ δ 𝑖 ⇒
-    comp A (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 };
+    comp A (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 }