From 629434c75245b38aa01444acb3145149deed4754 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 5 Jun 2023 16:42:11 +0200
Subject: [PATCH] wip maybe.quox

---
 examples/all.quox   |  1 +
 examples/maybe.quox | 69 +++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 70 insertions(+)
 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..ae1c12f
--- /dev/null
+++ b/examples/maybe.quox
@@ -0,0 +1,69 @@
+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)) →
+    ω.(ω.(x : A) → P (Just A x)) →
+    1.(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