From 5f6eab248d1d8da04c9bee314529c6375d831978 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 20 Oct 2023 05:25:57 +0200
Subject: [PATCH] qty.quox

---
 examples/qty.quox | 73 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 73 insertions(+)
 create mode 100644 examples/qty.quox

diff --git a/examples/qty.quox b/examples/qty.quox
new file mode 100644
index 0000000..26a1a8b
--- /dev/null
+++ b/examples/qty.quox
@@ -0,0 +1,73 @@
+def0 Qty : ★ = {"zero", one, any}
+
+def dup : Qty → [ω.Qty] =
+  λ π ⇒ case π return [ω.Qty] of {
+    'zero ⇒ ['zero];
+    'one  ⇒ ['one];
+    'any  ⇒ ['any];
+  }
+
+def drop : 0.(A : ★) → Qty → A → A =
+  λ A π x ⇒ case π return A of {
+    'zero ⇒ x;
+    'one  ⇒ x;
+    'any  ⇒ x;
+  }
+
+def if-zero : 0.(A : ★) → Qty → ω.A → ω.A → A =
+  λ A π z nz ⇒
+  case π return A of { 'zero ⇒ z; 'one ⇒ nz; 'any ⇒ nz }
+
+def plus : Qty → Qty → Qty =
+  λ π ρ ⇒
+  case π return Qty of {
+    'zero ⇒ ρ;
+    'one  ⇒ if-zero Qty ρ 'one 'any;
+    'any  ⇒ drop Qty ρ 'any;
+  }
+
+def times : Qty → Qty → Qty =
+  λ π ρ ⇒
+  case π return Qty of {
+    'zero ⇒ drop Qty ρ 'zero;
+    'one  ⇒ ρ;
+    'any  ⇒ if-zero Qty ρ 'zero 'any;
+  }
+
+def0 FUN : Qty → (A : ★) → (A → ★) → ★ =
+  λ π A B ⇒
+  case π return ★ of {
+    'zero ⇒ 0.(x : A) → B x;
+    'one  ⇒ 1.(x : A) → B x;
+    'any  ⇒ ω.(x : A) → B x;
+  }
+
+def0 Fun : Qty → ★ → ★ → ★ =
+  λ π A B ⇒ FUN π A (λ _ ⇒ B)
+
+def0 Box : Qty → ★ → ★ =
+  λ π A ⇒
+  case π return ★ of {
+    'zero ⇒ [0.A];
+    'one  ⇒ [1.A];
+    'any  ⇒ [ω.A];
+  }
+
+def0 unbox : (π : Qty) → (A : ★) → Box π A → A =
+  λ π A ⇒
+  case π return π' ⇒ Box π' A → A of {
+    'zero ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
+    'one  ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
+    'any  ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
+  }
+
+def apply : (π : Qty) → 0.(A : ★) → 0.(B : A → ★) →
+            FUN π A B → (x : Box π A) → B (unbox π A x) =
+  λ π A B ⇒
+  case π
+  return π' ⇒ FUN π' A B → (x : Box π' A) → B (unbox π' A x)
+  of {
+    'zero ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'zero A x') of { [x] ⇒ f x };
+    'one  ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'one  A x') of { [x] ⇒ f x };
+    'any  ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'any  A x') of { [x] ⇒ f x };
+  }