From 599744c7c54b39c29cc588d40a60c92c9ed254cd Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Sun, 17 Mar 2024 18:14:23 -0400 Subject: [PATCH 1/4] add some design documentation corresponding to issue #312. (Redo of bad 957) --- doc/README/Design/Miscellany.agda | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 doc/README/Design/Miscellany.agda diff --git a/doc/README/Design/Miscellany.agda b/doc/README/Design/Miscellany.agda new file mode 100644 index 0000000000..547bc69e7c --- /dev/null +++ b/doc/README/Design/Miscellany.agda @@ -0,0 +1,17 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Documentation describing some of the smaller choices in the library +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module README.Design.Miscellany where + +------------------------------------------------------------------------- +-- Level polymorphism + +-- `⊥` in `Data.Empty` and `⊤` in `Data.Unit` are not `Level`-polymorphic as that +-- tends to lead to unsolved metas (see discussion at issue #312). For that purpose, +-- there are now level-polymorphic version in `Data.Empty.Polymorphic` and +-- `Data.Unit.Polymorphic` respectively. From 2d2910078f5a518a1c56da1898043f48cc3ec306 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Mon, 25 Mar 2024 21:44:38 -0400 Subject: [PATCH 2/4] more documentation about LevelPolymorphism --- doc/README/Design/LevelPolymorphism.md | 11 +++++++++++ doc/README/Design/Miscellany.agda | 17 ----------------- 2 files changed, 11 insertions(+), 17 deletions(-) create mode 100644 doc/README/Design/LevelPolymorphism.md delete mode 100644 doc/README/Design/Miscellany.agda diff --git a/doc/README/Design/LevelPolymorphism.md b/doc/README/Design/LevelPolymorphism.md new file mode 100644 index 0000000000..0038d81944 --- /dev/null +++ b/doc/README/Design/LevelPolymorphism.md @@ -0,0 +1,11 @@ +* Level polymorphism + +`⊥` in `Data.Empty` and `⊤` in `Data.Unit` are not `Level`-polymorphic as that +tends to lead to unsolved metas (see discussion at issue #312). This is understandable +as very often the level of (say) `⊤` is under-determined by its surrounding context, +leading to unsolved metas. This is frequent enough that it makes sense for the default +versions to be monomorphic (at Level 0). + +But there are other cases where exactly the opposite is needed. for that purpose, +there are level-polymorphic versions in `Data.Empty.Polymorphic` and +`Data.Unit.Polymorphic` respectively. diff --git a/doc/README/Design/Miscellany.agda b/doc/README/Design/Miscellany.agda deleted file mode 100644 index 547bc69e7c..0000000000 --- a/doc/README/Design/Miscellany.agda +++ /dev/null @@ -1,17 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Documentation describing some of the smaller choices in the library ------------------------------------------------------------------------- - -{-# OPTIONS --cubical-compatible --safe #-} - -module README.Design.Miscellany where - -------------------------------------------------------------------------- --- Level polymorphism - --- `⊥` in `Data.Empty` and `⊤` in `Data.Unit` are not `Level`-polymorphic as that --- tends to lead to unsolved metas (see discussion at issue #312). For that purpose, --- there are now level-polymorphic version in `Data.Empty.Polymorphic` and --- `Data.Unit.Polymorphic` respectively. From 84d361eaf8c2c1504fa0ae1fa72971ba10674924 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Mon, 25 Mar 2024 21:48:24 -0400 Subject: [PATCH 3/4] more documentation precision --- src/Data/Empty.agda | 2 +- src/Data/Unit.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Empty.agda b/src/Data/Empty.agda index 990a9a1632..19754e8c7d 100644 --- a/src/Data/Empty.agda +++ b/src/Data/Empty.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Empty type, judgementally proof irrelevant +-- Empty type, judgementally proof irrelevant, Level-monomorphic ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} diff --git a/src/Data/Unit.agda b/src/Data/Unit.agda index 2e3464c7f4..73f269d9d6 100644 --- a/src/Data/Unit.agda +++ b/src/Data/Unit.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- The unit type +-- The unit type, Level-monomorphic version ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} From 58a0c0c827cfee7ed878bacb26af148faeed8eeb Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Tue, 26 Mar 2024 10:57:23 -0400 Subject: [PATCH 4/4] document issues wrt Relation.Unary, both in design doc and in file itself. --- doc/README/Design/LevelPolymorphism.md | 4 ++++ src/Relation/Unary.agda | 3 +++ 2 files changed, 7 insertions(+) diff --git a/doc/README/Design/LevelPolymorphism.md b/doc/README/Design/LevelPolymorphism.md index 0038d81944..59436fe4a3 100644 --- a/doc/README/Design/LevelPolymorphism.md +++ b/doc/README/Design/LevelPolymorphism.md @@ -9,3 +9,7 @@ versions to be monomorphic (at Level 0). But there are other cases where exactly the opposite is needed. for that purpose, there are level-polymorphic versions in `Data.Empty.Polymorphic` and `Data.Unit.Polymorphic` respectively. + +The same issue happens in `Relation.Unary` which defines `Ø` and `U` at `Level` 0, else +a lot of unsolved metas appear (for example in `Relation.Unary.Properties`). For that +purpose, `Relation.Unary.Polymorphic` exists. diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda index 9f3ea16633..0f8a7534fd 100644 --- a/src/Relation/Unary.agda +++ b/src/Relation/Unary.agda @@ -42,6 +42,8 @@ Pred A ℓ = A → Set ℓ -- Special sets -- The empty set. +-- Explicitly not level polymorphic as this often causes unsolved metas; +-- see `Relation.Unary.Polymorphic` for a level-polymorphic version. ∅ : Pred A 0ℓ ∅ = λ _ → ⊥ @@ -52,6 +54,7 @@ Pred A ℓ = A → Set ℓ ｛ x ｝ = x ≡_ -- The universal set. +-- Explicitly not level polymorphic (see comments for `∅` for more details) U : Pred A 0ℓ U = λ _ → ⊤