From e087b891558945e18d91850e3343fe06ba31d45b Mon Sep 17 00:00:00 2001 From: pmbittner Date: Wed, 3 Jul 2024 10:46:55 +0200 Subject: [PATCH 1/4] extend note on sized types We use them in a more restricted and sane way than previously reported. --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index a583d5cd..b138faf7 100644 --- a/README.md +++ b/README.md @@ -390,9 +390,10 @@ Proofs are documented inline via comments in the code (also see the Documentatio #### On Axioms and Assumptions -We use sized types, which currently have [known inconsistencies](https://github.com/agda/agda/issues/6002), for termination checking. +For termination checking, we use sized types, which currently have [known inconsistencies](https://github.com/agda/agda/issues/6002). The risks of using them in inconsistent ways are [often accepted](https://github.com/agda/agda/issues/4908) because they can simplify proofs substantially. We came to the same conclusion and tried our best to use them without interaction with more complicated language features to reduce the likelihood of encountering an inconsistency. +(In particular, we only use the plain inductive flavor `Size` with `↑_` and do not mix it with the `Size<_` type because it is especially mixing the two which is causing inconsistencies (in particular in case of the issue above).) Our library, does not use any of the following assumptions or axioms in central parts of the code: From 8cfbe04f93bc998725aa2f2ce4186ad5f672f372 Mon Sep 17 00:00:00 2001 From: pmbittner Date: Wed, 3 Jul 2024 10:48:55 +0200 Subject: [PATCH 2/4] delete deprecated SizeJuggle file To increase trust in us using sized types sanely. This file was definitely some madness. Fortunately, the module was not used anymore. --- src/Util/SizeJuggle.agda | 183 --------------------------------------- 1 file changed, 183 deletions(-) delete mode 100644 src/Util/SizeJuggle.agda diff --git a/src/Util/SizeJuggle.agda b/src/Util/SizeJuggle.agda deleted file mode 100644 index 936a355f..00000000 --- a/src/Util/SizeJuggle.agda +++ /dev/null @@ -1,183 +0,0 @@ -{- -Module with functions for assisting Agda's type checker -when it comes to checking sized types. -Sometimes we need to help a little with explicit type annotations -and safe casts. - -This module is called juggling because sometimes Agda can magically convert between the two independent types Size and Size< which we can never do manually. -But sometimes Agda fails. -We can help it with some id functions that have the right type signature though. --} -module Util.SizeJuggle where - --- to get ⊔ˢ type \lub\^s --- remember to press ^ button twice! -open import Size using (Size; SizeUniv; Size<_; ↑_; _⊔ˢ_) -open import Util.Existence using (∃-Size; _,_) -open import Data.List - using (List; []; _∷_) - renaming (map to mapl) -open import Data.List.NonEmpty - using (List⁺; _∷_; toList) - --- We consider a type as bounded if it is parameterized in a size. -Bounded : Set₁ -Bounded = Size → Set - -record Weaken (B : Bounded) : Set where - field - to-larger : ∀ (weaker-bound : Size) - (current-bound : Size< weaker-bound) - (e : B current-bound) - ------------------------------------ - → B weaker-bound - - -- we cannot build to-max from to-larger because the maximum is not strictly larger than either i or j. It is equal to one of them. - -- This is a result of not being able to prove i≤i⊔j (see above). - to-max : ∀ (i j : Size) - (e : B i) - ------------ - → B (i ⊔ˢ j) -open Weaken public - --- A size is smaller than itself + 1. -i<↑i : (i : Size) → Size< (↑ i) -i<↑i i = i - -i<↑max : ∀ (i j : Size) → Size< (↑ (i ⊔ˢ j)) -i<↑max i _ = i - -i<↑i-list : - (B : Bounded) - → (i : Size) - → List (B i) - → List (B (i<↑i i)) -i<↑i-list _ _ l = l - -data _≡ˢ_ (i : Size) : Size → Set where - instance reflˢ : i ≡ˢ i - -data _≤ˢ_ : Size → Size → Set where - equal : ∀ {i : Size} - ------ - → i ≤ˢ i - - smaller : ∀ {i : Size} - → {j : Size< i} - ------------- - → j ≤ˢ i - --- Equivalence is not decidable because we have no way to inspect a size. --- It is just an opaque name to us. --- _≟_ : ∀ (i j : Size) → Dec (i ≡ˢ j) - --- There is also no way to prove that sizes must be equal or one must be larger than the other one. --- i≤i⊔j : --- ∀ (i j : Size) --- -------------- --- → i ≤ˢ (i ⊔ˢ j) - -trans : (i : Size) (j : Size< i) (k : Size< j) → {- k is -} Size< i -trans i j k = k - - -weaken-by-1 : ∀ {B : Bounded} {i : Size} - → (Weaken B) - → (e : B i) - --------- - → B (↑ i) -weaken-by-1 {i = i} weaken e = to-larger weaken (↑ i) (i<↑i i) e - -weaken-to-↑max : ∀ {B : Bounded} - → (Weaken B) - → (i j : Size) - → B i - -------------- - → B (↑ (i ⊔ˢ j)) -weaken-to-↑max weaken i j e = - -- Version using to-larger instead of to-max - --to-larger weaken (↑ (i ⊔ˢ j)) (i<↑max i j) e - weaken-by-1 weaken (to-max weaken i j e) - -weaken-to-smaller-↑max : ∀ {B : Bounded} - → (Weaken B) - → (i j : Size) - → B i - → B (i<↑i (i ⊔ˢ j)) -weaken-to-smaller-↑max weaken = to-max weaken - -sym-max : ∀ {B : Bounded} {i j : Size} - → B (i ⊔ˢ j) - ---------- - → B (j ⊔ˢ i) -sym-max max = max - -sym-↑max : ∀ {B : Bounded} - → (i j : Size) - → B (↑ (i ⊔ˢ j)) - -------------- - → B (↑ (j ⊔ˢ i)) -sym-↑max _ _ max = max - -sym-smaller-↑max : - ∀ (B : Bounded) - → (i j : Size) - → B (i<↑i (i ⊔ˢ j)) - -------------- - → B (i<↑i (j ⊔ˢ i)) -sym-smaller-↑max _ _ _ max = max - --- Functions for Lists - -weaken-list : ∀ {B : Bounded} - → Weaken B - → (i : Size) - → (j : Size< i) - → List (B j) - ------------- - → List (B i) -weaken-list w i j l = mapl (to-larger w i j) l - -weaken-list-max : ∀ {B : Bounded} - → Weaken B - → (i j : Size) - → List (B i) - ----------------- - → List (B (i ⊔ˢ j)) -weaken-list-max w i j l = mapl (to-max w i j) l - -prepend-sized : ∀ {B : Bounded} - → Weaken B - → (i j : Size) - → B i - → List (B j) - ----------------- - → List (B (i ⊔ˢ j)) -prepend-sized {B} w i j h t = - let sized-head : B (i ⊔ˢ j) - sized-head = to-max w i j h - - sized-tail : List (B (i ⊔ˢ j)) - sized-tail = weaken-list-max w j i t - in - sized-head ∷ sized-tail - -{- -Given a list of individually sized expressions, we find the maximum size and cast every expression to that maximum size. In case the list is empty, the given default value is returned. --} -unify-sizes : ∀ {B : Bounded} - → Weaken B - → Size - → List (∃-Size[ i ] (B i)) - → ∃-Size[ max ] (List (B max)) -unify-sizes _ ε [] = ε , [] -unify-sizes w ε ((i , e) ∷ xs) = - let (max-tail , tail) = unify-sizes w ε xs - in i ⊔ˢ max-tail , prepend-sized w i max-tail e tail -- Why is there a warning highlight without a message here? - -{- -Same as max-size⁺ but for non-empty list. -We can thus be sure that a maximum size exist and do not need a default value. --} -unify-sizes⁺ : ∀ {B : Bounded} → Weaken B → List⁺ (∃-Size[ i ] (B i)) → ∃-Size[ max ] (List (B max)) -unify-sizes⁺ L list@((i , _) ∷ _) = unify-sizes L i (toList list) From 6ffe856e6b51418c727ba3ee5f4a634af78bec6e Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Wed, 3 Jul 2024 22:18:17 +0200 Subject: [PATCH 3/4] README: Provide a more general link for sized types inconsistencies --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index b138faf7..10db0d22 100644 --- a/README.md +++ b/README.md @@ -390,7 +390,7 @@ Proofs are documented inline via comments in the code (also see the Documentatio #### On Axioms and Assumptions -For termination checking, we use sized types, which currently have [known inconsistencies](https://github.com/agda/agda/issues/6002). +For termination checking, we use sized types, which currently have [known inconsistencies](https://github.com/agda/agda/issues?q=is%3Aopen+label%3Afalse+sized+types). The risks of using them in inconsistent ways are [often accepted](https://github.com/agda/agda/issues/4908) because they can simplify proofs substantially. We came to the same conclusion and tried our best to use them without interaction with more complicated language features to reduce the likelihood of encountering an inconsistency. (In particular, we only use the plain inductive flavor `Size` with `↑_` and do not mix it with the `Size<_` type because it is especially mixing the two which is causing inconsistencies (in particular in case of the issue above).) From 8f2839e925f20521244c62f7dab51968d3d9b905 Mon Sep 17 00:00:00 2001 From: pmbittner Date: Thu, 4 Jul 2024 00:13:30 +0200 Subject: [PATCH 4/4] README: refine reasoning on sized types --- README.md | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 10db0d22..4cdaac12 100644 --- a/README.md +++ b/README.md @@ -390,18 +390,13 @@ Proofs are documented inline via comments in the code (also see the Documentatio #### On Axioms and Assumptions -For termination checking, we use sized types, which currently have [known inconsistencies](https://github.com/agda/agda/issues?q=is%3Aopen+label%3Afalse+sized+types). -The risks of using them in inconsistent ways are [often accepted](https://github.com/agda/agda/issues/4908) because they can simplify proofs substantially. -We came to the same conclusion and tried our best to use them without interaction with more complicated language features to reduce the likelihood of encountering an inconsistency. -(In particular, we only use the plain inductive flavor `Size` with `↑_` and do not mix it with the `Size<_` type because it is especially mixing the two which is causing inconsistencies (in particular in case of the issue above).) - Our library, does not use any of the following assumptions or axioms in central parts of the code: 1. **no** additional axioms via `postulate` (e.g., no extensionality or excluded middle) 2. **no** termination macros (`{-# TERMINATING -#}`). All functions and proofs are proven to terminate (for proofs this means they use well-founded induction or are non-cyclic). 3. **no** unfinished proofs (i.e., there are no holes `{! !}`). -Of course, there are two exceptions to this. +Of course, there are three exceptions to this. ##### Exception 1 @@ -413,6 +408,16 @@ of the library multiple times, by using sized types. ##### Exception 2 +For termination checking, we use sized types, which currently have [known inconsistencies](https://github.com/agda/agda/issues?q=is%3Aopen+label%3Afalse+sized+types). +The risks of using them in inconsistent ways are [often accepted](https://github.com/agda/agda/issues/4908) because they can simplify proofs substantially. +We came to the same conclusion and tried our best to use them without interaction with more complicated language features to reduce the likelihood of encountering an inconsistency. +In particular, we use sized types only in a very basic, inductive way and: +- We do not use coinductive data types ([#7178](https://github.com/agda/agda/issues/7178), [#1946](https://github.com/agda/agda/issues/1946), [#1201](https://github.com/agda/agda/issues/1201)). +- We do not use `Size<` ([#6002](https://github.com/agda/agda/issues/6002)). +- We do not compare `Size` for equality ([#2820](https://github.com/agda/agda/issues/2820)). + +##### Exception 3 + For a non-crucial part of our framework, we included four postulates, which assume that two primitive operations from the standard library are invertible: - converting `String`s to lists of characters and vice versa