From f4d56bc5cbd5aacabd737085149fa0188abc0623 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Mon, 3 Jun 2024 01:03:09 -0400 Subject: [PATCH] blog: write one more --- aya/blog/extended-pruning.md | 100 +++++++++++++++++++++++++++++++ aya/guide/prover-tutorial.aya.md | 5 +- package.json | 2 +- pnpm-lock.yaml | 36 +++++------ src/.vitepress/config.mts | 1 + 5 files changed, 123 insertions(+), 21 deletions(-) create mode 100644 aya/blog/extended-pruning.md diff --git a/aya/blog/extended-pruning.md b/aya/blog/extended-pruning.md new file mode 100644 index 0000000..bce443a --- /dev/null +++ b/aya/blog/extended-pruning.md @@ -0,0 +1,100 @@ +# Extended pruning for pattern unification + +The vanilla pattern unification is very limited. +Consider + +```aya-hidden +prim I prim coe prim Path +variable A B : Type +def infix = (a b : A) => Path (\i => A) a b +def refl {a : A} : a = a => fn i => a + +open inductive Nat +| zero +| suc Nat +overlap def infix + Nat Nat : Nat +| 0, n => n +| n, 0 => n +| suc m, n => suc (m + n) +| m, suc n => suc (m + n) +tighter = +def pmap (f : A -> B) {a b : A} (p : a = b) : f a = f b + => fn i => f (p i) +variable n m o : Nat +variable i : I +// Definitions +open inductive Vec (n : Nat) (A : Type) +| 0, A => nil +| suc n, A => infixr :< A (Vec n A) +overlap def infixr ++ (Vec n A) (Vec m A) : Vec (n + m) A +| nil, ys => ys +| ys, nil => ys +| x :< xs, ys => x :< xs ++ ys +tighter :< = +def +-assoc {a b c : Nat} : (a + b) + c = a + (b + c) elim a +| 0 => refl +| suc _ => pmap suc +-assoc +def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A) + => +``` + +```aya + PathP (fn i => Vec (+-assoc i) A) + (xs ++ (ys ++ zs)) + ((xs ++ ys) ++ zs) +``` + +This is the equality between two sized vectors: `(xs ++ (ys ++ zs))` and `((xs ++ ys) ++ zs)`, +the left hand side has type `Vec (xs.size ++ (ys.size ++ zs.size)) A`, +and the right hand side has type `Vec ((xs.size ++ ys.size) ++ zs.size)`. + +So, the equality type is heterogeneous, and I introduce a type `Vec (+-assoc i) A`{} for it, where `+-assoc`{} is the associativity. + +So this should type check, right? But pattern unification fails! I've left the two sides of `+-assoc`{} implicit, +so I'm supposed to infer what numbers' associativity I care about, using pattern unification. + +Then, pattern unification _fails_ because the constraints are generated from cubical boundaries, +where the "interval" variable is substituted to its sides. So, we have this type +(the `Path`{} is called `PathP` in Agda): + +``` +Γ ­⊢ Path (fn i => Vec (+-assoc i) Nat) vecA vecB +``` + +Note the type of `+-assoc`{} is `+-assoc`{show=type}. + +So elaboration inserts metavariables: + +``` +Γ ­⊢ Path (fn i => Vec (+-assoc {?} {?} {?} i) Nat) vecA vecB +``` + +Where these metavariables have the following scope: + +``` +Γ , i : I ­⊢ ? : Nat +``` + +Note that the `i : I` binding is in-scope. So the metavariables with their spines added together becomes: + +``` +Γ ­⊢ Path (fn i => Vec (+-assoc {?a Γ i} {?b Γ i} {?c Γ i} i) Nat) vecA vecB +``` + +Then, we get the following tycking problems, according to the rules of PathP: + +``` +vecA : Vec (+-assoc {?a Γ 0} {?b Γ 0} {?c Γ 0} 0) Nat +vecB : Vec (+-assoc {?a Γ 1} {?b Γ 1} {?c Γ 1} 0) Nat +``` + +Look at the spines of all of these metavariables. None of them are in pattern fragment. +So _every_ equality constraint cannot be solved by pattern, because they're always equality _after a substitution_! + +This can be solved by further extending your algorithm with pruning or a constraint system with a "lax" +mode of solving metas when your equations rely essentially on non-pattern equations, +but I feel it has defeated the point of finding the most general solution, +which I used to believe to be the purpose of pattern unification.... + +Right now Aya will try to prune these non-pattern arguments out and try to solve them. +This obviously generates non-unique solutions, but I think it will be useful in practice. diff --git a/aya/guide/prover-tutorial.aya.md b/aya/guide/prover-tutorial.aya.md index 2d33672..f9c67ef 100644 --- a/aya/guide/prover-tutorial.aya.md +++ b/aya/guide/prover-tutorial.aya.md @@ -69,8 +69,9 @@ def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g ``` This is because Aya has a "cubical" equality type that is not inductively defined. -An equality `a = b` for `a, b : A` is really just a function `I -> A` where `I` is a special type -carrying two values around. +An equality `a = b` for `a, b : A` is really just a function `I -> A`{} where `I`{} +is a special type carrying two values around (there's supposed to be a short +introduction to cubical ideas here, but I don't have time to write that out yet). We may also prove the action-on-path theorem, commonly known as `cong`, but renamed to `pmap`{} to avoid a potential future naming clash: diff --git a/package.json b/package.json index d29c5d6..94a6ced 100644 --- a/package.json +++ b/package.json @@ -1,7 +1,7 @@ { "name": "aya-prover-docs", "version": "1.0.0", - "packageManager": "pnpm@9.1.2", + "packageManager": "pnpm@9.1.4", "description": "The documentation site of the Aya prover.", "main": "index.js", "scripts": { diff --git a/pnpm-lock.yaml b/pnpm-lock.yaml index e6893c6..0cb9f1e 100644 --- a/pnpm-lock.yaml +++ b/pnpm-lock.yaml @@ -502,11 +502,11 @@ packages: cpu: [x64] os: [win32] - '@shikijs/core@1.6.1': - resolution: {integrity: sha512-CqYyepN4SnBopaoXYwng4NO8riB5ask/LTCkhOFq+GNGtr2X+aKeD767eYdqYukeixEUvv4bXdyTYVaogj7KBw==} + '@shikijs/core@1.6.2': + resolution: {integrity: sha512-guW5JeDzZ7uwOjTfCOFZ2VtVXk5tmkMzBYbKGfXsmAH1qYOej49L5jQDcGmwd6/OgvpmWhzO2GNJkQIFnbwLPQ==} - '@shikijs/transformers@1.6.1': - resolution: {integrity: sha512-m/h2Dh99XWvTzHL8MUQmEnrB+/gxDljIfgDNR00Zg941KENqORx8Hi9sKpGYjCgXoEJKASZlEMQdPnkHj9/8aQ==} + '@shikijs/transformers@1.6.2': + resolution: {integrity: sha512-ndqTWyHnxmsLkowhKWTam26opw8hg5a34y6FAUG/Xf6E49n3MM//nenKxXiWpPYkNPl1KZnYXB1k+Ia46wjOZg==} '@types/estree@1.0.5': resolution: {integrity: sha512-/kYRxGDLWzHOB7q+wtSUQlFrtcdUccpfy+X+9iMBpHK8QLLhx2wIPYuS5DYtR9Wa/YlZAbIovy7qVdB1Aq6Lyw==} @@ -665,8 +665,8 @@ packages: resolution: {integrity: sha512-Gmy6FhYlCY7uOElZUSbxo2UCDH8owEk996gkbrpsgGtrJLM3J7jGxl9Ic7Qwwj4ivOE5AWZWRMecDdF7hqGjFA==} engines: {node: '>=10'} - caniuse-lite@1.0.30001626: - resolution: {integrity: sha512-JRW7kAH8PFJzoPCJhLSHgDgKg5348hsQ68aqb+slnzuB5QFERv846oA/mRChmlLAOdEDeOkRn3ynb1gSFnjt3w==} + caniuse-lite@1.0.30001627: + resolution: {integrity: sha512-4zgNiB8nTyV/tHhwZrFs88ryjls/lHiqFhrxCW4qSTeuRByBVnPYpDInchOIySWknznucaf31Z4KYqjfbrecVw==} chalk@2.4.2: resolution: {integrity: sha512-Mti+f9lpJNcwF4tWV8/OrTTtF1gZi+f8FqlyAdouralcFWFQWF2+NgCHShjkCb+IFBLq9buZwE1xckQU4peSuQ==} @@ -821,8 +821,8 @@ packages: resolution: {integrity: sha512-BR7VvDCVHO+q2xBEWskxS6DJE1qRnb7DxzUrogb71CWoSficBxYsiAGd+Kl0mmq/MprG9yArRkyrQxTO6XjMzA==} hasBin: true - shiki@1.6.1: - resolution: {integrity: sha512-1Pu/A1rtsG6HZvQm4W0NExQ45e02og+rPog7PDaFDiMumZgOYnZIu4JtGQeAIfMwdbKSjJQoCUr79vDLKUUxWA==} + shiki@1.6.2: + resolution: {integrity: sha512-X3hSm5GzzBd/BmPmGfkueOUADLyBoZo1ojYQXhd+NU2VJn458yt4duaS0rVzC+WtqftSV7mTVvDw+OB9AHi3Eg==} source-map-js@1.2.0: resolution: {integrity: sha512-itJW8lvSA0TXEphiRoawsCksnlf8SyvmFzIhltqAHluXd88pkCd+cXJVHTDwdCr0IzwptSm035IHQktUu1QUMg==} @@ -1366,11 +1366,11 @@ snapshots: '@rollup/rollup-win32-x64-msvc@4.18.0': optional: true - '@shikijs/core@1.6.1': {} + '@shikijs/core@1.6.2': {} - '@shikijs/transformers@1.6.1': + '@shikijs/transformers@1.6.2': dependencies: - shiki: 1.6.1 + shiki: 1.6.2 '@types/estree@1.0.5': {} @@ -1563,14 +1563,14 @@ snapshots: browserslist@4.23.0: dependencies: - caniuse-lite: 1.0.30001626 + caniuse-lite: 1.0.30001627 electron-to-chromium: 1.4.788 node-releases: 2.0.14 update-browserslist-db: 1.0.16(browserslist@4.23.0) camelcase@6.3.0: {} - caniuse-lite@1.0.30001626: {} + caniuse-lite@1.0.30001627: {} chalk@2.4.2: dependencies: @@ -1719,9 +1719,9 @@ snapshots: semver@6.3.1: {} - shiki@1.6.1: + shiki@1.6.2: dependencies: - '@shikijs/core': 1.6.1 + '@shikijs/core': 1.6.2 source-map-js@1.2.0: {} @@ -1755,8 +1755,8 @@ snapshots: dependencies: '@docsearch/css': 3.6.0 '@docsearch/js': 3.6.0(@algolia/client-search@4.23.3)(search-insights@2.14.0) - '@shikijs/core': 1.6.1 - '@shikijs/transformers': 1.6.1 + '@shikijs/core': 1.6.2 + '@shikijs/transformers': 1.6.2 '@types/markdown-it': 14.1.1 '@vitejs/plugin-vue': 5.0.5(vite@5.2.12)(vue@3.4.27) '@vue/devtools-api': 7.2.1(vue@3.4.27) @@ -1766,7 +1766,7 @@ snapshots: focus-trap: 7.5.4 mark.js: 8.11.1 minisearch: 6.3.0 - shiki: 1.6.1 + shiki: 1.6.2 vite: 5.2.12 vue: 3.4.27 optionalDependencies: diff --git a/src/.vitepress/config.mts b/src/.vitepress/config.mts index f9ecd7e..5a4ded2 100644 --- a/src/.vitepress/config.mts +++ b/src/.vitepress/config.mts @@ -42,6 +42,7 @@ export default defineConfig({ { text: 'Blog', items: [ + { text: 'Extended Pruning', link: '/blog/extended-pruning' }, { text: 'Farewell, Univalence', link: '/blog/bye-hott' }, { text: 'Inductive Props', link: '/blog/ind-prop' }, { text: 'Def. projection in classes', link: '/blog/class-defeq' },