agda-stdlib
agda-stdlib copied to clipboard
Deprecate old function hierarchy
I propose the following two backwards compatible additions.
(1) To add to Function.Injection
InjectiveBy≡ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
InjectiveBy≡ f = ∀ {x y} → f x ≡ f y → x ≡ y
To add to Function.Surjection
SurjectiveBy≡ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
SurjectiveBy≡ {_} {_} {_} {B} f = (y : B) → ∃ (\x → f x ≡ y)
To add to Function.Bijection
BijectiveBy≡ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
BijectiveBy≡ f = InjectiveBy≡ f × SurjectiveBy≡ f
(2) To reexport In(Sur,Bi)jective, In(Sur,Bi)jectiveBy≡
from Function
.
Motivation.
(2) is proposed because it is nicer to write a single ... import Function using (...)
instead of the four import decls:
Function, Function.Injection, Function.Surjection, Function.Bijection.
(1) is proposed because In(Sur,Bi)jectiveBy≡
have a wide application area and also are simple to perceive and to use, while the generic In(Sur,Bi)jective
are declared so that they are difficult to perceive and to use.
If the user really needs the general version, all right, let him study the general constructs given there by record
s.
The problem I can see with these definitions is that we would now have two (essentially the same on propositional equality) distinct notions of injectivity and we would need to convert between them.
We already have "smart constructors" for injectivity involving propositional equality, would that solve your problem? https://agda.github.io/agda-stdlib/Function.Injection.html#1399
For example, consider
suc-injective : ∀ {m n} → suc m ≡ suc n → m ≡ n
suc-injective refl = refl
in Data.Nat.Properties. Why does not it use Injective
? Can you demonstrate the usage of smart constructors for suc-injective : Injective suc
?
Now, I suggest the following.
------------------------------------------------------------ Function/GenericInjSurBi.agda ---------
module Function.GenericInjSurBi where
...
module _ {ℓ ℓ= ℓ' ℓ'=} (From : Setoid ℓ ℓ=) (To : Setoid ℓ' ℓ'=)
where
open Setoid From using () renaming (Carrier to A; _≈_ to _≈_)
open Setoid To using () renaming (Carrier to B; _≈_ to _≈'_)
GenericInjective : Pred (A → B) _
GenericInjective f = ∀ {x y} → f x ≈' f y → x ≈ y
GenericSurjective : Pred (A → B) _
GenericSurjective f = (y : B) → ∃ (\x → f x ≈' y)
GenericBijective : Pred (A → B) _
GenericBijective f = GenericInjective f × GenericSurjective f
module _ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'}
where
InjectiveBy≡ SurjectiveBy≡ BijectiveBy≡ : Pred (A → B) _
InjectiveBy≡ = GenericInjective (PE.setoid A) (PE.setoid B)
SurjectiveBy≡ = GenericSurjective (PE.setoid A) (PE.setoid B)
BijectiveBy≡ = GenericBijective (PE.setoid A) (PE.setoid B)
-----------------------------------------------------------------------------------------------------------------
Example of usage: put to Data.Nat.Properties
open import Function.GenericInjSurBi using (InjectiveBy≡)
suc-injective : InjectiveBy≡ suc
suc-injective refl = refl
GenericInjective
co-exists with Injective
of lib-1.0 and also is more generic. Because if cf
is a congruent map between setoids, then in can be derived
GenericInjective f
for f : Carrier₁ → Carrier₂
extracted from cf
-- probably it can be extracted.
(I never used Injective
of lib-1.0 and do not know how is it arranged, and what constructors to use).
A similar relation is for Surjective and Bijective.
In most situations the users will use GenericIn(Sur,Bi)jective
or In(Sur,Bi)jectiveBy≡
.
In the remaining situations let them use In(Sur,Bi)jective
by lib-1.0.
Also I would like to rename GenericInjective
to Injective
,
and to rename Injective
of lib-1.0 to something -- if you can agree with this breaking backwards compatibility.
If anything should be done to the function hierarchy then it should be made more consistent with other record hierarchies (e.g. IsInjection
/Injection
). Obviously this is fairly non-backwards compatible. I'm currently not sure how this would interact with the current design of exposing the setoids directly.
I agree with @mechvel though that they should be exported by Function
directly.
Can you point concretely, may be with example: what harm can do using the above GenericInjective
or InjectiveBy≡
?
I have shown the advantage, now, please, show a drawback.
For any occasion: I am not in a hurry, I can wait long for people to return from holydays and to concentrate on the answer. I post things in the process, because if I delay the post, then I would deal with another subjects and probably forget of the issue.
Can you point concretely, may be with example: what harm can do using the above GenericInjective or InjectiveBy≡ ? I have shown the advantage, now, please, show a drawback.
The problem is one of long-term drawbacks rather than short-term drawbacks. The end goal should be to make the library consistent and therefore easy to use. At the moment the function hierarchy does not follow the same rules as the other hierarchies in the library, and this discourages users from using it, as you yourself said.
The problem with your proposal is that it would add further non-standard names that do not obey the IsX
/X
convention. This creates further work in the future when we get around to fixing the hierarchy. I agree with the problems you have identified, but I'm not sure your proposed solution is the right long-term way to go about fixing it.
I'm afraid tackling the function hierarchy isn't on anyone's immediate list of priorities at the moment as far as I'm aware, but I'll leave the issue open as a reminder.
I'm afraid tackling the function hierarchy isn't on anyone's immediate list of priorities
I do not know precisely whether I am in the anyone list, but for any occasion, let me name my top priorities relatively to Standard.
- The features named in the announcement of BFLib-0.1 and implemented there: generic definition of divisibility, gcd, generic fraction arithmetic, a full item set for Bin.
- Certified arithmetic of natural numbers represented as lists of macro-digits.
What is function hierarchy? For example, are the matters of a generic definition of divisibility and gcd, generic definition of a fraction (see BFLib) of function hierarchy ?
As to GenericInjective, the proposals for standard can easily avoid this issue at all. For example, to write everywhere things like
suc-injective : ∀ {m n} → suc m ≡ suc n → m ≡ n
foo-injective : ∀ {x y} → foo x ≈' foo y → x ≈ y
The result will be that no user would set the words Injective, Surjective, Bijective
of standard to the type expressions.
What is function hierarchy? For example, are the matters of a generic definition of divisibility and gcd, generic definition of a fraction (see BFLib) of function hierarchy ?
See in README.agda
https://github.com/agda/agda-stdlib/blob/f1368a6541aae6328159e6c8ea4eb7d40fe0c5d0/README.agda#L166-L168 .
The examples you give above are therefore not part of the function hierarchy.
As to GenericInjective, the proposals for standard can easily avoid this issue at all. For example, to write everywhere things like. ... The result will be that no user would set the words Injective, Surjective, Bijective of standard to the type expressions.
As I said above, I agree it's a problem that there's no easy-to-use definitions for Injective
, Surjective
etc. in the library, but I don't think GenericInjective
is the way to go. What I have in mind is:
module _ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} where
Injective : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
Injective _≈_ _≈′_ f = ∀ {x y} → f x ≈′ f y → x ≈ y
record IsInjection (_≈_ : Rel A ℓ₁) (_≈′_ : Rel B ℓ₂)
(f : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
cong : f Preserves _≈_ ⟶ _≈′_
injective : Injective _≈_ _≈′_ f
record Injection : Set (a ⊔ b ⊔ suc ℓ₁ ⊔ suc ℓ₂) where
field
_≈_ : Rel A ℓ₁
_≈′_ : Rel B ℓ₂
f : A → B
isInjection : IsInjection _≈_ _≈′_ f
This follows the same record hierarchy as in Algebra
and Relation.Binary
. The proof of injectivity could then be written as:
suc-injective : Injective _≡_ _≡_ suc
suc-injective refl = refl
Obviously what to do with the existing code is problematic. We could move them to a separate sub-directory Function.Setoid
.
This is better than Injective
of lib-1.0. The drawback is pushed one level down.
The matter is that for a theory with equality injectivity has sense not only for congruent maps
(I can give a simple example), and its code is simpler to use.
The code will be nicer and more usable if the library delays as possible introducing the congruence condition. Say,
Injection = Σ (A → B) (Injective _≈_ _≈′_)
And the corresponding definitions for congruent maps can be obtained by joining the above definitions with the condition of Congruent f
, with also inserting the "Cong" word somewhere to the name of the predicate.
(?)
Also it is desirable to avoid records for simple definitions (?)
-- because the field names usually cause the necessity of renaming. For example, this cong
will clash with PropositionalEquality.cong
, which creeps in almost everywhere.
If you call this field differently, then its meaning will not be so easily understood.
Similarly, _∣_
looks better and is used easier when it is defined as ∃ (\q → a ≈ q ∙ b)
.
Modules that have functionality that needs to be transferred across:
Core functionality
A lot of stuff in these modules has been ported, but modules are not marked completed until all of it is has.
- [x] src/Function/Equality.agda
- [x] Missing an indexed function variant. Should go in a new hierarchy
Function.Dependent.(Structures/Bundles)
- [x]
setoid
inFunction.Indexed.Relation.Binary.Equality
- [x]
≡-setoid
- [x]
flip
- [x] Missing an indexed function variant. Should go in a new hierarchy
- [x] src/Function/Injection.agda
- [x] src/Function/Surjection.agda
- [x]
fromRightInverse
(should probably go in a new moduleFunction.Properties.RightInverse
)
- [x]
- [x] src/Function/Bijection.agda
- [x] src/Function/Inverse.agda
- [x]
_↔̇_
(what even is that weird character above the arrow?) - [x]
fromBijection
(should probably go in a new moduleFunction.Properties.Bijection
) - [ ]
map
(under some sort ofFunction.Construct.X
module? Does this operation generalise to other function structures?) - [ ]
zip
(under some sort ofFunction.Construct.X
module? Does this operation generalise to other function structures?)
- [x]
- [x] src/Function/LeftInverse.agda
- [x] src/Function/HalfAdjointEquivalence (not even bundles/structures done yet)
Dependencies
Unless stated otherwise most of these are simply copying the definitions and updating them to use the new hierarhcy.
Easy
- [x] src/Algebra/Construct/LiftedChoice.agda
- [x] src/Data/List/Countdown.agda
- [x] src/Data/Fin/Properties.agda
- [x] src/Data/Nat/Properties.agda
Moderate
- [x] src/Data/List/Membership/Propositional/Properties.agda
- [x] src/Data/Product/Function/NonDependent/Setoid.agda
- [x] src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
- [x] src/Data/Product/Function/NonDependent/Propositional.agda
- [x] src/Data/Sum/Function/Setoid.agda
- [x] src/Data/Sum/Function/Propositional.agda
- [x] src/Relation/Nullary/Decidable.agda
- [x] src/Function/Related.agda (should be relatively simple, need to define alternative mappings for each kind)
- [x] src/Function/Related/TypeIsomorphisms (I think this has already been done by @JacquesCarette in
Data.(Sum/Product).Algebra
.)
Hard
Uses dependent functions, which we don't yet have a hierarchy for (see comment on Function.Equality
above)
- [x] src/Data/Product/Function/Dependent/Setoid.agda
- [x] src/Data/Product/Function/Dependent/Setoid/WithK.agda
- [x] src/Data/Product/Function/Dependent/Propositional.agda
- [x] src/Data/Product/Function/Dependent/Propositional/WithK.agda
I've got two new summer students, and I've asked them to start their work on stdlib here. Expect PRs 'soon'.
Hi! Glad to be here! Just to make sure I got this right -
agda-stdlib
used to have a particular structure for the Function
module (or package?) which wasn't very user friendly. This issue aims to restructure the module in such a way that the imports make more sense to the users and the developers.
So there are two sides here -
- Migrating the actual code to a different location
- Updating the
Function
imports or dependencies in other packages/modules
In a future major release, the following modules will disappear completely -
Function.Equivalence
Function.Equality
Function.Bijection
Function.Injection
Function.Surjection
Function.LeftInverse
and maybe even more.
If I did get this right, I am currently trying to migrate fromBijection
from Function.Inverse
to Function.Properties.Bijection
. I am getting some errors while running the tests locally and I am debugging them at the moment. I might require some help in debugging the failures, will create a PR shortly with more information.
Yes, that's essentially correct. It's probably a good idea to start new issues for discussion of each sub-part (when needed), otherwise this issue is going to "blow up" in size (it's already quite long). Debugging help is definitely best asked for on Zulip and other messaging sites.
Great! Thank you so much! I'll redirect all the debugging questions to Zulip or Discord.
Based on some digging and a discussion on zulip, I think the following can be crossed off the list -
-
fromRightInverse
-
fromBijection
- src/Function/Related.agda
- src/Function/Surjection.agda
- ~src/Relation/Nullary/Decidable.agda~ maybe not this
Thanks @Saransh-cpp for the help! Feel free to cross them off if you find they're already done.
So I've got a PR open that does some of this already (https://github.com/agda/agda-stdlib/pull/1895). In particular:
- src/Data/Product/Function/Dependent/Setoid.agda
- src/Data/Product/Function/Dependent/Setoid/WithK.agda
- src/Data/Product/Function/Dependent/Propositional.agda
- src/Data/Product/Function/Dependent/Propositional/WithK.agda
However, it ended up blocked on https://github.com/agda/agda-stdlib/pull/1156. Hopefully that should be merged in sometime this week.