agda-stdlib

agda-stdlib copied to clipboard

When reexporting things, there are sometimes type signatures stated in comments. I think I found a few places where these type signatures are inaccurate, for example:

https://github.com/agda/agda-stdlib/blob/ebfb8814b4330b314da8fb9cae527e6a6fab01aa/src/Data/Nat/Properties.agda#L1196

This function actually takes the n argument first and the m argument second, because x≤y⊔x is a renaming of x⊓y≤y which of course takes the x argument first: https://github.com/agda/agda-stdlib/blob/ebfb8814b4330b314da8fb9cae527e6a6fab01aa/src/Algebra/Construct/NaturalChoice/MinOp.agda#L43

The same issue is present in all four places where x≤y⊔x is re-exported:

src/Data/Integer/Properties.agda:  ; x≤y⊔x     to i≤j⊔i        -- : ∀ i j → i ≤ j ⊔ i
src/Data/Nat/Properties.agda:  ; x≤y⊔x     to m≤n⊔m        -- : ∀ m n → m ≤ n ⊔ m
src/Data/Rational/Properties.agda:  ; x≤y⊔x     to p≤q⊔p        -- : ∀ p q → p ≤ q ⊔ p
src/Data/Rational/Unnormalised/Properties.agda:  ; x≤y⊔x      to p≤q⊔p          -- : ∀ p q → p ≤ q ⊔ p

The same thing happens for example for x≤y⇒x≤z⊔y (which is a renaming of x≤y⇒z⊓x≤y), but here only the order of the implicit arguments is flipped:

src/Data/Integer/Properties.agda:  ; x≤y⇒x≤z⊔y to i≤j⇒i≤k⊔j    -- : ∀ {i j} k → i ≤ j → i ≤ k ⊔ j
src/Data/Nat/Properties.agda:  ; x≤y⇒x≤z⊔y to m≤n⇒m≤o⊔n    -- : ∀ {m n} o → m ≤ n → m ≤ o ⊔ n
src/Data/Rational/Properties.agda:  ; x≤y⇒x≤z⊔y to p≤q⇒p≤r⊔q    -- : ∀ {p q} r → p ≤ q → p ≤ r ⊔ q
src/Data/Rational/Unnormalised/Properties.agda:  ; x≤y⇒x≤z⊔y  to p≤q⇒p≤r⊔q      -- : ∀ {p q} r → p ≤ q → p ≤ r ⊔ q

Thank you, nice spot! Wish these weren't necessary and we had editor support...

I wonder if it could be best here to change the actual type signatures of x≤y⊔x and x≤y⇒x≤z⊔y (and similar cases) to reflect the order in which the variables x, y, z appear in the name.

In your "I wonder", do you mean that the rename

  ; x⊓y≤y      to x≤y⊔x

should instead be

  ; x⊓y≤y      to y≤x⊔y

?

No, I meant that there should be this:

x≤y⊔x : ∀ x y → x ≤ y ⊔ x

This can not be achieved by a renaming-reexport of x⊓y≤y, one would need a separate definition to flip the arguments.

Also, n≤m⊔n was deprecated and m≤n⊔m was introduced -

https://github.com/agda/agda-stdlib/blob/0661b59be0ccf28d5715d80fd9e6c535ed19d119/src/Data/Nat/Properties.agda#L2261-L2264

Should I just update the type signature in the comments?

We bumped this from v2.0 to v2.1... suggest we do so again to v2.2 unless someone feels like tackling this before the end of June?