Skip to content

Qualified imports in Data.Integer.Divisibility fixing #2280 #2294

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Mar 3, 2024
Merged

Qualified imports in Data.Integer.Divisibility fixing #2280 #2294

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a1785ae
fixing #2280
jamesmckinna Feb 14, 2024
3025f3f
re-export constructor via pattern synonym
jamesmckinna Feb 14, 2024
b2e2cf1
updated `README`
jamesmckinna Feb 14, 2024
39608f7
refactor: better disambiguation; added a note in `CHANGELOG`
jamesmckinna Feb 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,11 @@ Additions to existing modules
nonZeroIndex : Fin n → ℕ.NonZero n
```

* In `Data.Integer.Divisisbility`: introduce `divides` as an explicit pattern synonym
```agda
pattern divides k eq = Data.Nat.Divisibility.divides k eq
```

* In `Data.List.Relation.Unary.All.Properties`:
```agda
All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
Expand Down
16 changes: 8 additions & 8 deletions doc/README/Data/Integer.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,29 +33,29 @@ ex₃ = + 1 + + 3 * - + 2 - + 4
-- Propositional equality and some related properties can be found
-- in Relation.Binary.PropositionalEquality.

open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

ex₄ : ex₃ ≡ - + 9
ex₄ = P.refl
ex₄ = ≡.refl

-- Data.Integer.Properties contains a number of properties related to
-- integers. Algebra defines what a commutative ring is, among other
-- things.

import Data.Integer.Properties as ℤₚ
import Data.Integer.Properties as ℤ

ex₅ : ∀ i j → i * j ≡ j * i
ex₅ i j = ℤₚ.*-comm i j
ex₅ i j = ℤ.*-comm i j

-- The module ≡-Reasoning in Relation.Binary.PropositionalEquality
-- provides some combinators for equational reasoning.

open P.≡-Reasoning
open ≡.≡-Reasoning

ex₆ : ∀ i j → i * (j + + 0) ≡ j * i
ex₆ i j = begin
i * (j + + 0) ≡⟨ P.cong (i *_) (ℤₚ.+-identityʳ j) ⟩
i * j ≡⟨ ℤₚ.*-comm i j ⟩
i * (j + + 0) ≡⟨ ≡.cong (i *_) (ℤ.+-identityʳ j) ⟩
i * j ≡⟨ ℤ.*-comm i j ⟩
j * i ∎

-- The module RingSolver in Data.Integer.Solver contains a solver
Expand All @@ -67,4 +67,4 @@ open +-*-Solver

ex₇ : ∀ i j → i * - j - j * i ≡ - + 2 * i * j
ex₇ = solve 2 (λ i j → i :* :- j :- j :* i := :- con (+ 2) :* i :* j)
P.refl
≡.refl
20 changes: 10 additions & 10 deletions src/Data/Integer/Divisibility.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,42 +14,42 @@ open import Function.Base using (_on_; _$_)
open import Data.Integer.Base
open import Data.Integer.Properties
import Data.Nat.Base as ℕ
import Data.Nat.Divisibility as ℕᵈ
import Data.Nat.Divisibility as ℕ
open import Level
open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
open import Relation.Binary.PropositionalEquality


------------------------------------------------------------------------
-- Divisibility

infix 4 _∣_

_∣_ : Rel ℤ 0ℓ
_∣_ = ℕᵈ._∣_ on ∣_∣
_∣_ = ℕ._∣_ on ∣_∣

open ℕᵈ public using (divides)
pattern divides k eq = ℕ.divides k eq
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are we sure that this doesn't cause clashes if people have both Data.Nat.Divisibility and Data.Integer.Divisibility in scope?

Copy link
Contributor Author

@jamesmckinna jamesmckinna Feb 15, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, in some sense, I think it is worse than that, in that it will cause clashes (unless there's something I don't understand), so this is perhaps Not The Right Answer.

That said, I would worry about any context in which each of Data.Nat.Divisibility and Data.Integer.Divisibility were in scope unqualified, because this would cause a separate (dis-)ambiguation problem wrt the relation symbol _|_ itself.

In fact, Data.Integer.Divisibility.Signed does import both modules, but qualified, in the service of defining, and proving properties of, _|_ on the signed representation of ℤ, which also introduces divides as a constructor...! And that does work fine, because each module is imported qualified, and indeed, the imported constructor is used only in two places, in the definitions of ∣ᵤ⇒∣ and ∣⇒∣ᵤ ;-) My PR currently disambiguates the pun on divides by reusing ℕ.divides in those definitions, but (of course!?) using Unsigned.divides works as well, and perhaps better 'respects the abstraction barrier' at play here.

And indeed, in the spirit of other 'style' comments, I've simplified a complicated qualified import with a using and a renaming directive, in favour of a simpler qualified import and then using it in place to appropriately disambiguate the puns.

I think the existing (legacy) design is a hack to 'overload'/'borrow' the constructor for one definition, that of _|_ on ℕ, and turn it into a constructor for _|_ on ℤ. This is fine (I don't like it, but meh; puns considered harmful as a programming idiom) on the current model of untyped patterns/pattern synonyms. But I think that if we ever move to a typed model of pattern matching, then this shouldn't be OK? (or could it be?)

The problem, as I understand it, is to find a way to 'export' the constructor, for the (unsigned) Integer.Divisibility context, in such a way that it is type-correct for the definition of _|_ on ℤ. My solution, which I admit I perhaps did not think hard enough about, nor long enough, was to make this 'shallow' copy, and to use qualified import to explicitly disambiguate. But I'm not sure I know how to do better than the original, in my view hacky, design. Advice welcome!

Copy link
Contributor Author

@jamesmckinna jamesmckinna Feb 15, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Committed the 'better' disambiguation, and a note in CHANGELOG.

But that doesn't resolve the question of whether this is the 'right' way to solve the problem... client modules (none in stdlib) which exploit the pun on import will break, I guess, so I'll add the breaking label?

UPDATED: and, unfortunately, it's still a breaking change (but perhaps a 'lesser' one) not to introduce the synonym at all (and revert to the use of ℕ.divides in Data.Integer.Divisibility.Signed), which I had also, briefly, considered, until thinking "clients might still need/expect/want to see that constructor in scope; yuk!"... ;-)

Copy link
Contributor Author

@jamesmckinna jamesmckinna Feb 15, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Half-way house: put a {-# WARNING_ON_USAGE #-} for divides (*not* a deprecation per se) in favour of ℕ.divides for v2.1, and then make the breaking change in v3.0?

The imports in ...Signed can be fixed as in the PR, and this would leave a hint to downstream clients to migrate their code ahead of v3.0?


------------------------------------------------------------------------
-- Properties of divisibility

*-monoʳ-∣ : ∀ k → (k *_) Preserves _∣_ ⟶ _∣_
*-monoʳ-∣ k {i} {j} i∣j = begin
∣ k * i ∣ ≡⟨ abs-* k i ⟩
∣ k ∣ ℕ.* ∣ i ∣ ∣⟨ ℕᵈ.*-monoʳ-∣ ∣ k ∣ i∣j ⟩
∣ k ∣ ℕ.* ∣ j ∣ ≡⟨ sym (abs-* k j) ⟩
∣ k ∣ ℕ.* ∣ i ∣ ∣⟨ ℕ.*-monoʳ-∣ ∣ k ∣ i∣j ⟩
∣ k ∣ ℕ.* ∣ j ∣ ≡⟨ abs-* k j ⟨
∣ k * j ∣ ∎
where open ℕᵈ.∣-Reasoning
where open ℕ.∣-Reasoning

*-monoˡ-∣ : ∀ k → (_* k) Preserves _∣_ ⟶ _∣_
*-monoˡ-∣ k {i} {j} rewrite *-comm i k | *-comm j k = *-monoʳ-∣ k

*-cancelˡ-∣ : ∀ k {i j} .{{_ : NonZero k}} → k * i ∣ k * j → i ∣ j
*-cancelˡ-∣ k {i} {j} k*i∣k*j = ℕᵈ.*-cancelˡ-∣ ∣ k ∣ $ begin
∣ k ∣ ℕ.* ∣ i ∣ ≡⟨ sym (abs-* k i) ⟩
*-cancelˡ-∣ k {i} {j} k*i∣k*j = ℕ.*-cancelˡ-∣ ∣ k ∣ $ begin
∣ k ∣ ℕ.* ∣ i ∣ ≡⟨ abs-* k i ⟨
∣ k * i ∣ ∣⟨ k*i∣k*j ⟩
∣ k * j ∣ ≡⟨ abs-* k j ⟩
∣ k ∣ ℕ.* ∣ j ∣ ∎
where open ℕᵈ.∣-Reasoning
where open ℕ.∣-Reasoning

*-cancelʳ-∣ : ∀ k {i j} .{{_ : NonZero k}} → i * k ∣ j * k → i ∣ j
*-cancelʳ-∣ k {i} {j} rewrite *-comm i k | *-comm j k = *-cancelˡ-∣ k
14 changes: 6 additions & 8 deletions src/Data/Integer/Divisibility/Signed.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,7 @@ module Data.Integer.Divisibility.Signed where
open import Function.Base using (_⟨_⟩_; _$_; _$′_; _∘_; _∘′_)
open import Data.Integer.Base
open import Data.Integer.Properties
open import Data.Integer.Divisibility as Unsigned
using (divides)
renaming (_∣_ to _∣ᵤ_)
import Data.Integer.Divisibility as Unsigned
import Data.Nat.Base as ℕ
import Data.Nat.Divisibility as ℕ
import Data.Nat.Coprimality as ℕ
Expand Down Expand Up @@ -45,9 +43,9 @@ open _∣_ using (quotient) public
------------------------------------------------------------------------
-- Conversion between signed and unsigned divisibility

∣ᵤ⇒∣ : ∀ {k i} → k ∣ᵤ i → k ∣ i
∣ᵤ⇒∣ {k} {i} (divides 0 eq) = divides (+ 0) (∣i∣≡0⇒i≡0 eq)
∣ᵤ⇒∣ {k} {i} (divides q@(ℕ.suc _) eq) with k ≟ +0
∣ᵤ⇒∣ : ∀ {k i} → k Unsigned.∣ i → k ∣ i
∣ᵤ⇒∣ {k} {i} (Unsigned.divides 0 eq) = divides (+ 0) (∣i∣≡0⇒i≡0 eq)
∣ᵤ⇒∣ {k} {i} (Unsigned.divides q@(ℕ.suc _) eq) with k ≟ +0
... | yes refl = divides +0 (∣i∣≡0⇒i≡0 (trans eq (ℕ.*-zeroʳ q)))
... | no neq = divides (sign i Sign.* sign k ◃ q) (◃-cong sign-eq abs-eq)
where
Expand Down Expand Up @@ -85,8 +83,8 @@ open _∣_ using (quotient) public
∣ i ∣ ∎
where open ≡-Reasoning

∣⇒∣ᵤ : ∀ {k i} → k ∣ i → k ∣ᵤ i
∣⇒∣ᵤ {k} {i} (divides q eq) = divides ∣ q ∣ $′ begin
∣⇒∣ᵤ : ∀ {k i} → k ∣ i → k Unsigned.∣ i
∣⇒∣ᵤ {k} {i} (divides q eq) = Unsigned.divides ∣ q ∣ $′ begin
∣ i ∣ ≡⟨ cong ∣_∣ eq ⟩
∣ q * k ∣ ≡⟨ abs-* q k ⟩
∣ q ∣ ℕ.* ∣ k ∣ ∎
Expand Down
3 changes: 1 addition & 2 deletions src/Data/Integer/GCD.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,9 @@ module Data.Integer.GCD where
open import Data.Integer.Base
open import Data.Integer.Divisibility
open import Data.Integer.Properties
open import Data.Nat.Base
import Data.Nat.GCD as ℕ
open import Data.Product.Base using (_,_)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)

open import Algebra.Definitions {A = ℤ} _≡_ as Algebra
using (Associative; Commutative; LeftIdentity; RightIdentity; LeftZero; RightZero; Zero)
Expand Down
3 changes: 1 addition & 2 deletions src/Data/Integer/LCM.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,8 @@ module Data.Integer.LCM where
open import Data.Integer.Base
open import Data.Integer.Divisibility
open import Data.Integer.GCD
open import Data.Nat.Base using (ℕ)
import Data.Nat.LCM as ℕ
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)

------------------------------------------------------------------------
-- Definition
Expand Down