From b4a8438434e2b6ccd5a4302dd417f3e9e1ed1b09 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 19 Apr 2023 00:42:40 +0200 Subject: [PATCH] examples --- examples/bool.quox | 29 ++++++++++++ examples/either.quox | 76 ++++++++++++++++++++++++------- examples/list.quox | 12 +++-- examples/misc.quox | 41 ++++++++--------- examples/nat.quox | 106 +++++++++++++++++++++++++++++++++++++------ examples/pair.quox | 52 +++++++++++++++++++++ 6 files changed, 260 insertions(+), 56 deletions(-) create mode 100644 examples/bool.quox create mode 100644 examples/pair.quox diff --git a/examples/bool.quox b/examples/bool.quox new file mode 100644 index 0000000..d4c5de3 --- /dev/null +++ b/examples/bool.quox @@ -0,0 +1,29 @@ +load "misc.quox"; + +namespace bool { + +def0 Bool : ★₀ = {true, false}; + +def boolω : 1.Bool → [ω.Bool] = + λ b ⇒ case1 b return [ω.Bool] of { 'true ⇒ ['true]; 'false ⇒ ['false] }; + +def if : 0.(A : ★₀) → 1.Bool → ω.A → ω.A → A = + λ A b t f ⇒ case1 b return A of { 'true ⇒ t; 'false ⇒ f }; + +-- [todo]: universe lifting +def0 If : 1.Bool → 0.★₀ → 0.★₀ → ★₀ = + λ b T F ⇒ case1 b return ★₀ of { 'true ⇒ T; 'false ⇒ F }; + +def0 T : ω.Bool → ★₀ = λ b ⇒ If b True False; + +def true-not-false : Not ('true ≡ 'false : Bool) = + λ eq ⇒ coe [i ⇒ T (eq @i)] @0 @1 'true; + + +-- [todo] infix +def and : ω.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false; +def or : ω.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b; + +} + +def0 Bool = bool.Bool; diff --git a/examples/either.quox b/examples/either.quox index 8c060dd..45f5c23 100644 --- a/examples/either.quox +++ b/examples/either.quox @@ -1,32 +1,76 @@ +load "misc.quox"; +load "bool.quox"; + +namespace either { + def0 Tag : ★₀ = {left, right}; -def0 Payload : 0.(A : ★₀) → 0(B : .★₀) → 1.Tag → ★₀ = +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 = +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 = +def Right : 0.(A : ★₀) → 0.(B : ★₀) → 1.B → Either A B = λ A B x ⇒ ('right, x); -defω either-elim : +def 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.(t : Tag) → 1.(a : Payload A B t) → P (t, a) = + λ A B P f g t ⇒ + case1 t + return t' ⇒ 1.(a : Payload A B t') → P (t', a) + of { 'left ⇒ f; 'right ⇒ g }; + +def 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) - }; + λ A B P f g e ⇒ + case1 e return e' ⇒ P e' of { (t, a) ⇒ elim' A B P f g t a }; + + +} + +def0 Either = either.Either; +def Left = either.Left; +def Right = either.Right; + + +namespace dec { + +def0 Dec : 0.★₀ → ★₀ = λ A ⇒ Either [0.A] [0.Not A]; + +def Yes : 0.(A : ★₀) → 0.A → Dec A = λ A y ⇒ Left [0.A] [0.Not A] [y]; +def No : 0.(A : ★₀) → 0.(Not A) → Dec A = λ A n ⇒ Right [0.A] [0.Not A] [n]; + +def0 DecEq : 0.★₀ → ★₀ = + λ A ⇒ ω.(x : A) → ω.(y : A) → Dec (x ≡ y : A); + +def elim : + 0.(A : ★₀) → 0.(P : 0.(Dec A) → ★₀) → + ω.(0.(y : A) → P (Yes A y)) → + ω.(0.(n : Not A) → P (No A n)) → + 1.(x : Dec A) → P x = + λ A P f g ⇒ + either.elim [0.A] [0.Not A] P + (λ y ⇒ case0 y return y' ⇒ P (Left [0.A] [0.Not A] y') of {[y'] ⇒ f y'}) + (λ n ⇒ case0 n return n' ⇒ P (Right [0.A] [0.Not A] n') of {[n'] ⇒ g n'}); + +def bool : 0.(A : ★₀) → 1.(Dec A) → Bool = + λ A ⇒ elim A (λ _ ⇒ Bool) (λ _ ⇒ 'true) (λ _ ⇒ 'false); + +} + +def0 Dec = dec.Dec; +def0 DecEq = dec.DecEq; +def Yes = dec.Yes; +def No = dec.No; diff --git a/examples/list.quox b/examples/list.quox index e7c5f6e..5fe605e 100644 --- a/examples/list.quox +++ b/examples/list.quox @@ -1,3 +1,7 @@ +load "nat.quox"; + +namespace list { + def0 Vec : 0.ℕ → 0.★₀ → ★₀ = λ n A ⇒ caseω n return ★₀ of { @@ -29,10 +33,10 @@ def foldr : 0.(A : ★₀) → 0.(B : ★₀) → λ A B z c xs ⇒ case1 xs return B of { (len, elems) ⇒ foldr' A B z c len elems }; -load "nat.quox"; +def sum : 1.(List ℕ) → ℕ = foldr ℕ ℕ 0 nat.plus; -def sum : 1.(List ℕ) → ℕ = foldr ℕ ℕ 0 plus; - -def numbers : List ℕ = (5, (0, 1, 2, 3, 4, 5, 'nil)); +def numbers : List ℕ = (5, (0, 1, 2, 3, 4, 'nil)); def number-sum : sum numbers ≡ 10 : ℕ = δ _ ⇒ 10; + +} diff --git a/examples/misc.quox b/examples/misc.quox index ef2a31b..2c87e2a 100644 --- a/examples/misc.quox +++ b/examples/misc.quox @@ -1,14 +1,22 @@ +def0 True : ★₀ = {true}; + +def0 False : ★₀ = {}; +def0 Not : 0.★₀ → ★₀ = λ A ⇒ ω.A → False; + +def void : 0.(A : ★₀) → 0.False → A = + λ A v ⇒ case0 v return A of { }; + def0 Pred : 0.★₀ → ★₁ = λ A ⇒ 0.A → ★₀; def0 All : 0.(A : ★₀) → 0.(Pred A) → ★₁ = λ A P ⇒ 1.(x : A) → P x; -defω cong : +def cong : 0.(A : ★₀) → 0.(P : Pred A) → 1.(p : All A P) → 0.(x : A) → 0.(y : A) → 1.(xy : x ≡ y : A) → - Eq [i ⇒ P (xy @i)] (p x) (p y) = - λ A P p x y xy ⇒ δ i ⇒ p (xy @i); + Eq [𝑖 ⇒ P (xy @𝑖)] (p x) (p y) = + λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖); def0 eq-f : 0.(A : ★₀) → 0.(P : Pred A) → @@ -16,27 +24,18 @@ def0 eq-f : 0.A → ★₀ = λ A P p q x ⇒ p x ≡ q x : P x; -defω funext : +def funext : 0.(A : ★₀) → 0.(P : Pred A) → 0.(p : All A P) → 0.(q : All A P) → 1.(All A (eq-f A P p q)) → p ≡ q : All A P = - λ A P p q eq ⇒ δ i ⇒ λ x ⇒ eq x @i; + λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖; -def0 T : ω.{true, false} → ★₀ = - λ b ⇒ caseω b return ★₀ of { 'true ⇒ {tt}; 'false ⇒ {} }; +def sym : 0.(A : ★₀) → 0.(x : A) → 0.(y : A) → + 1.(x ≡ y : A) → y ≡ x : A = + λ A x y eq ⇒ δ 𝑖 ⇒ comp [A] @0 @1 (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 }; -defω absurd : - 0.('true ≡ 'false : {true, false}) → 0.(A : ★₀) → A = - λ eq A ⇒ - case0 coe [i ⇒ T (eq @i)] @0 @1 'tt return A of { }; - -defω sym : 0.(A : ★₀) → 0.(x : A) → 0.(y : A) → - 1.(x ≡ y : A) → y ≡ x : A = - λ A x y eq ⇒ δ i ⇒ - comp [A] @0 @1 (eq @0) @i { 0 j ⇒ eq @j; 1 _ ⇒ eq @0 }; - -defω trans : 0.(A : ★₀) → 0.(x : A) → 0.(y : A) → 0.(z : A) → - ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A = - λ A x y z eq1 eq2 ⇒ δ i ⇒ - comp [A] @0 @1 (eq1 @i) @i { 0 _ ⇒ eq1 @0; 1 j ⇒ eq2 @j }; +def trans : 0.(A : ★₀) → 0.(x : A) → 0.(y : A) → 0.(z : A) → + ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A = + λ A x y z eq1 eq2 ⇒ δ 𝑖 ⇒ + comp [A] @0 @1 (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 }; diff --git a/examples/nat.quox b/examples/nat.quox index c72a3bf..6fbe4f0 100644 --- a/examples/nat.quox +++ b/examples/nat.quox @@ -1,9 +1,14 @@ -def dup-ℕ : 1.ℕ → [ω.ℕ] = +load "misc.quox"; +load "bool.quox"; +load "either.quox"; + +namespace nat { + +def dup : 1.ℕ → [ω.ℕ] = λ n ⇒ case1 n return [ω.ℕ] of { - zero ⇒ [zero]; - succ _, 1.d ⇒ - case1 d return [ω.ℕ] of { [d] ⇒ [succ d] } + zero ⇒ [zero]; + succ _, 1.d ⇒ case1 d return [ω.ℕ] of { [d] ⇒ [succ d] } }; def plus : 1.ℕ → 1.ℕ → ℕ = @@ -13,7 +18,7 @@ def plus : 1.ℕ → 1.ℕ → ℕ = succ _, 1.p ⇒ succ p }; -def times-ω : 1.ℕ → ω.ℕ → ℕ = +def timesω : 1.ℕ → ω.ℕ → ℕ = λ m n ⇒ case1 m return ℕ of { zero ⇒ zero; @@ -21,18 +26,89 @@ def times-ω : 1.ℕ → ω.ℕ → ℕ = }; def times : 1.ℕ → 1.ℕ → ℕ = - λ m n ⇒ - case1 dup-ℕ n return ℕ of { - [n] ⇒ times-ω m n - }; + λ m n ⇒ case1 dup n return ℕ of { [n] ⇒ timesω m n }; -def pred : 1.ℕ → ℕ = - λ n ⇒ - case1 n return ℕ of { zero ⇒ zero; succ n ⇒ n }; +def pred : 1.ℕ → ℕ = λ n ⇒ case1 n return ℕ of { zero ⇒ zero; succ n ⇒ n }; -def0 pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ = - λ n ⇒ δ i ⇒ n; +def pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ = + λ n ⇒ δ 𝑖 ⇒ n; def0 succ-inj : 0.(m : ℕ) → 0.(n : ℕ) → 0.(succ m ≡ succ n : ℕ) → m ≡ n : ℕ = - λ m n eq ⇒ δ i ⇒ pred (eq @i); + λ m n eq ⇒ δ 𝑖 ⇒ pred (eq @𝑖); + + +def0 IsSucc : 0.ℕ → ★₀ = + λ n ⇒ caseω n return ★₀ of { zero ⇒ False; succ _ ⇒ True }; + +def isSucc? : ω.(n : ℕ) → Dec (IsSucc n) = + λ n ⇒ + caseω n return n' ⇒ Dec (IsSucc n') of { + zero ⇒ No (IsSucc zero) (λ v ⇒ v); + succ n ⇒ Yes (IsSucc (succ n)) 'true + }; + +def zero-not-succ : 0.(m : ℕ) → Not (zero ≡ succ m : ℕ) = + λ m eq ⇒ coe [𝑖 ⇒ IsSucc (eq @𝑖)] @1 @0 'true; + +def succ-not-zero : 0.(m : ℕ) → Not (succ m ≡ zero : ℕ) = + λ m eq ⇒ coe [𝑖 ⇒ IsSucc (eq @𝑖)] @0 @1 'true; + + +def0 not-succ-self : 0.(m : ℕ) → Not (m ≡ succ m : ℕ) = + λ m ⇒ + caseω m return m' ⇒ Not (m' ≡ succ m' : ℕ) of { + zero ⇒ zero-not-succ 0; + succ n, ω.ih ⇒ λ eq ⇒ ih (succ-inj n (succ n) eq) + } + + +def eq? : DecEq ℕ = + λ m ⇒ + caseω m + return m' ⇒ ω.(n : ℕ) → Dec (m' ≡ n : ℕ) + of { + zero ⇒ λ n ⇒ + caseω n return n' ⇒ Dec (zero ≡ n' : ℕ) of { + zero ⇒ Yes (zero ≡ zero : ℕ) (δ _ ⇒ zero); + succ n' ⇒ No (zero ≡ succ n' : ℕ) (λ eq ⇒ zero-not-succ n' eq) + }; + succ m', ω.ih ⇒ λ n ⇒ + caseω n return n' ⇒ Dec (succ m' ≡ n' : ℕ) of { + zero ⇒ No (succ m' ≡ zero : ℕ) (λ eq ⇒ succ-not-zero m' eq); + succ n' ⇒ + dec.elim (m' ≡ n' : ℕ) (λ _ ⇒ Dec (succ m' ≡ succ n' : ℕ)) + (λ y ⇒ Yes (succ m' ≡ succ n' : ℕ) (δ 𝑖 ⇒ succ (y @𝑖))) + (λ n ⇒ No (succ m' ≡ succ n' : ℕ) (λ eq ⇒ n (succ-inj m' n' eq))) + (ih n') + } + }; + +def eqb : 1.ℕ → 1.ℕ → Bool = λ m n ⇒ dec.bool (m ≡ n : ℕ) (eq? m n); + + +def0 plus-zero : 0.(m : ℕ) → m ≡ plus m 0 : ℕ = + λ m ⇒ + caseω m return m' ⇒ m' ≡ plus m' 0 : ℕ of { + zero ⇒ δ _ ⇒ zero; + succ _, ω.ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖) + }; + +def0 plus-succ : 0.(m : ℕ) → 0.(n : ℕ) → succ (plus m n) ≡ plus m (succ n) : ℕ = + λ m n ⇒ + caseω m return m' ⇒ succ (plus m' n) ≡ plus m' (succ n) : ℕ of { + zero ⇒ δ _ ⇒ succ n; + succ _, ω.ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖) + }; + +def0 plus-comm : 0.(m : ℕ) → 0.(n : ℕ) → plus m n ≡ plus n m : ℕ = + λ m n ⇒ + caseω m return m' ⇒ plus m' n ≡ plus n m' : ℕ of { + zero ⇒ plus-zero n; + succ m', ω.ih ⇒ + trans ℕ (succ (plus m' n)) (succ (plus n m')) (plus n (succ m')) + (δ 𝑖 ⇒ succ (ih @𝑖)) + (plus-succ n m') + }; + +} diff --git a/examples/pair.quox b/examples/pair.quox new file mode 100644 index 0000000..8eee382 --- /dev/null +++ b/examples/pair.quox @@ -0,0 +1,52 @@ +namespace pair { + +def0 Σ : 0.(A : ★₀) → 0.(0.A → ★₀) → ★₀ = λ A B ⇒ (x : A) × B x; + +def fst : 0.(A : ★₀) → 0.(B : 0.A → ★₀) → + ω.(Σ A B) → A = + λ A B p ⇒ caseω p return A of { (x, _) ⇒ x }; + +def snd : 0.(A : ★₀) → 0.(B : 0.A → ★₀) → + ω.(p : Σ A B) → B (fst A B p) = + λ A B p ⇒ caseω p return p' ⇒ B (fst A B p') of { (_, y) ⇒ y }; + +def uncurry : + 0.(A : ★₀) → 0.(B : 0.A → ★₀) → 0.(C : 0.(x : A) → 0.(B x) → ★₀) → + 1.(f : 1.(x : A) → 1.(y : B x) → C x y) → + 1.(p : Σ A B) → C (fst A B p) (snd A B p) = + λ A B C f p ⇒ + case1 p return p' ⇒ C (fst A B p') (snd A B p') of { (x, y) ⇒ f x y }; + +def curry : + 0.(A : ★₀) → 0.(B : 0.A → ★₀) → 0.(C : 0.(Σ A B) → ★₀) → + 1.(f : 1.(p : Σ A B) → C p) → 1.(x : A) → 1.(y : B x) → C (x, y) = + λ A B C f x y ⇒ f (x, y); + +def0 fst-snd : + 0.(A : ★₀) → 0.(B : 0.A → ★₀) → + 1.(p : Σ A B) → p ≡ (fst A B p, snd A B p) : Σ A B = + λ A B p ⇒ + case1 p + return p' ⇒ p' ≡ (fst A B p', snd A B p') : Σ A B + of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) }; + +def map : + 0.(A : ★₀) → 0.(A' : ★₀) → + 0.(B : 0.A → ★₀) → 0.(B' : 0.A' → ★₀) → + 1.(f : 1.A → A') → 1.(g : 0.(x : A) → 1.(B x) → B' (f x)) → + 1.(Σ A B) → Σ A' B' = + λ A A' B B' f g p ⇒ + case1 p return Σ A' B' of { (x, y) ⇒ (f x, g x y) }; + +def map' : + 0.(A : ★₀) → 0.(A' : ★₀) → + 0.(B : ★₀) → 0.(B' : ★₀) → + 1.(f : 1.A → A') → 1.(g : 1.B → B') → + 1.(A × B) → A' × B' = + λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g); + +} + +def0 Σ = pair.Σ; +def fst = pair.fst; +def snd = pair.snd;