From 13e9285becda46a97aebac9efc91b1c17eb98274 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 31 Mar 2023 19:31:49 +0200
Subject: [PATCH] some examples [that don't work yet]

---
 examples/either.quox | 32 ++++++++++++++++
 examples/list.quox   | 89 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 121 insertions(+)
 create mode 100644 examples/either.quox
 create mode 100644 examples/list.quox

diff --git a/examples/either.quox b/examples/either.quox
new file mode 100644
index 0000000..8c060dd
--- /dev/null
+++ b/examples/either.quox
@@ -0,0 +1,32 @@
+def0 Tag : ★₀ = {left, right};
+
+def0 Payload : 0.(A : ★₀) → 0(B : .★₀) → 1.Tag → ★₀ =
+  λ A B tag ⇒ case1 tag return ★₀ of { 'left ⇒ A; 'right ⇒ B };
+
+def0 Either : 0.★₀ → 0.★₀ → ★₀ =
+  λ A B ⇒ (tag : Tag) × Payload A B tag;
+
+defω Left : 0.(A : ★₀) → 0.(B : ★₀) → 1.A → Either A B =
+  λ A B x ⇒ ('left, x);
+
+defω Right : 0.(A : ★₀) → 0.(B : ★₀) → 1.B → Either A B =
+  λ A B x ⇒ ('right, x);
+
+defω either-elim :
+    0.(A : ★₀) → 0.(B : ★₀) →
+    0.(P : 0.(Either A B) → ★₀) →
+    ω.(1.(x : A) → P (Left  A B x)) →
+    ω.(1.(x : B) → P (Right A B x)) →
+    1.(x : Either A B) → P x =
+  λ A B P f g x ⇒
+    case1 x return x' ⇒ P x' of {
+      (tag, value) ⇒
+        (case1 tag
+         return tag' ⇒
+           0.(eq : (tag ≡ tag' : Tag)) →
+           P (tag, coerce [i ⇒ Payload A B (eq i)] @0 @1 value)
+         of {
+           'left  ⇒ λ eq ⇒ f value;
+           'right ⇒ λ eq ⇒ g value
+         }) (δ _ ⇒ tag)
+    };
diff --git a/examples/list.quox b/examples/list.quox
new file mode 100644
index 0000000..5940ef4
--- /dev/null
+++ b/examples/list.quox
@@ -0,0 +1,89 @@
+
+def0 Vec : 0.ℕ → 0.★₀ → ★₀ =
+  λ n A ⇒
+  caseω n return ★₀ of {
+    zero           ⇒ {nil};
+    succ _, 0.Tail ⇒ A × Tail
+  };
+
+def0 List : 0.★₀ → ★₀ =
+  λ A ⇒ (len : ℕ) × Vec len A;
+
+
+defω nil : 0.(A : ★₀) → List A =
+  λ A ⇒ (0, 'nil);
+
+defω S : 1.ℕ → ℕ = λ n ⇒ succ n;
+
+defω cons : 0.(A : ★₀) → 1.A → 1.(List A) → List A =
+  λ A x xs ⇒
+  case1 xs return List A of {
+    (len, elems) ⇒ (succ len, x, elems)
+  };
+
+{-
+-- needs coercions overall,
+-- and real w-types to be linear
+defω list-ind :
+    0.(A : ★₀) →
+    0.(P : ω.(List A) → ★₀) →
+    1.(n : P (nil A)) →
+    ω.(c : 1.(x : A) → 0.(xs : List A) → 1.(P xs) → P (cons A x xs)) →
+    1.(lst : List A) → P lst =
+  λ A P n c lst ⇒
+    case1 lst return l ⇒ P l of {
+      (len, elems) ⇒
+        case1 len return len' ⇒ P (len', elems) of {
+          zero ⇒ n;
+          succ len', 1.ih ⇒
+            case1 elems return P (succ len', elems) of {
+              (first, rest) ⇒ c first rest ih
+            }
+        }
+    };
+
+defω foldr :
+    0.(A : ★₀) → 0.(B : ★₀) →
+    1.(n : B) → ω.(c : 1.A → 1.B → B) →
+    1.(List A) → B =
+  λ A B n c lst ⇒ list-ind A (λ _ ⇒ B) n (λ a as b ⇒ c a b) lst;
+
+-- ...still does
+defω foldr :
+    0.(A : ★₀) → 0.(B : ★₀) →
+    ω.(n : B) → ω.(c : 1.A → 1.B → B) →
+    ω.(List A) → B =
+  λ A B n c lst ⇒
+    caseω lst return B of {
+      (len, elems) ⇒
+        caseω len return B of {
+          zero ⇒ caseω elems return B of { 'nil ⇒ n };
+          succ _, ω.ih ⇒
+            caseω elems return B of {
+              (first, rest) ⇒ c first ih
+            }
+        }
+    };
+-}
+
+defω plus : 1.ℕ → 1.ℕ → ℕ =
+  λ m n ⇒
+  case1 m return ℕ of {
+    zero         ⇒ n;
+    succ _, 1.mn ⇒ succ mn
+  };
+
+-- case-ℕ's qout needs to be Σz + ωΣs
+
+def0 plus-3-3 : plus 3 3 ≡ 6 : ℕ =
+  δ 𝑖 ⇒ 6;
+
+{-
+defω sum : ω.(List ℕ) → ℕ = foldr ℕ ℕ 0 plus;
+
+defω numbers : List ℕ =
+  (5, (0, 1, 2, 3, 4, 'nil));
+
+defω number-sum : sum numbers ≡ 10 : ℕ =
+  δ _ ⇒ 10;
+-}