An alternative to generalised implication in Relation.Binary.Core?

[m0davis]

I find the following definition useful.

_⇒[_]=_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
          Rel A ℓ₁ → (B → A) → Rel B ℓ₂ → Set _
P ⇒[ f ]= Q = (P on f) ⇒ Q

It looks quite similar to generalised implication (or _Preserves_⟶_) from Relation.Binary.Core but I don't find the above definition there.

My current use-case is _×_ ⇒[ MyDatatype ]= _≡_. If there is a more clever way to write this using the standard library as-is, I'd be happy if someone pointed it out to me.

Would it make sense for me to make a pull request to add it? I'm somewhat unsure about the name. The ⇒ looks a bit strange to me sitting on the left-hand side. If it were to be added, I would figure we would need synonyms similar to Preserves et al. But again, I'm unsure how to name them.

[MatthewDaggitt]

Quite possibly though I'm a little confused about your use case. Could you expand it for a concrete datatype? I've tried letting "MyDatatype"=List and I'm not coming up with something useful, but maybe I'm just not seeing it.

[m0davis]

Here's a MWE of what I'm trying to do:

-- ** common stuff

open import Function
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core

_⇒[_]=_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
          Rel A ℓ₁ → (B → A) → Rel B ℓ₂ → Set _
P ⇒[ f ]= Q = (P on f) ⇒ Q

-- ** Nat stuff

open import Data.Nat

variable
  m n s : ℕ

-- ** particular datatype stuff here

-- my datatype (an encoding of summation)
data Add : ℕ → ℕ → ℕ → Set where
  zero : Add zero m m
  suc : Add n m s → Add (suc n) m (suc s)

-- a proof that Add is functional
≡-from-Add : _×_ ⇒[ Add n m ]= _≡_
≡-from-Add (zero , zero) = refl
≡-from-Add (suc add1 , suc add2) rewrite ≡-from-Add (add1 , add2) = refl

add = _+_ -- just a renaming here for brevity, but you can imagine I might have written a new function

-- creating `Add`s on-the-fly
runAdd : Add n m (add n m)
runAdd {zero} = zero
runAdd {suc n} = suc runAdd

Add is the datatype version of _+_. I like to define datatypes for many of the functions that I reason about because I find it tedious to use with and inspect. I place these functional datatypes in the constructors of larger (non-functional) datatypes instead of writing something like add n m ≡ k. Then, when I reason about the larger datatype, I find it convenient that I can case split on something like Add n m k. A downside to this method is in the proliferation of code (though I imagine I could use reflection to generate the necessary functions from the datatype).

[m0davis]

Here are two more use-cases, coming directly out of Data.Nat.Properties:

≤′-step-injective-from-stdlib : _≡_ ⇒[ ≤′-step {m} {n} ]= _≡_ -- N.B. generalised variables
≤′-step-injective-from-stdlib refl = refl

≤-pred-from-stdlib : _≤_ ⇒[ suc ]= _≤_
≤-pred-from-stdlib (s≤s m≤n) = m≤n

[MatthewDaggitt]

Ah okay, that makes sense. Yup, it would be fine to open a PR. As for names I'm okay with your suggestion though I agree it's a little strange. To be honest I think the existing notation for _=[_]⇒_ is a bit strange as well. Not sure if anyone else has any suggestions?

[andreasabel]

I do not find the MWE very compelling, since the following also works, and it is only a few keystrokes more:

≡-from-Add : (_×_ on Add n m) ⇒  _≡_

The most natural naming would then be _on[_]⇒_:

P on[ f ]⇒ Q = (P on f) ⇒ Q
...
≡-from-Add : _×_ on[ Add n m ]⇒  _≡_

But I am not very convinced this is above the Fairbairn threshold.
https://mail.haskell.org/pipermail/libraries/2012-February/017548.html

Tentatively closing, feel free to reopen and continue the discussion.

[m0davis]

If _on[_]⇒_ is below the Fairbairn threshold, then what of _[_]⇒_ (aka _Preserves_⟶_)? Shouldn't they either both be included or both be excluded from the stdlib?

Fwiw, if _on[_]⇒_ were to be included, I suggest that _[_]⇒_ be renamed to _[_]on⇒_.

[m0davis]

@andreasabel and/or @MatthewDaggitt, thoughts?

Btw, I would have reopened the issue but github does not give me that option.

[MatthewDaggitt]

Apologies for the delay in replying, I've been away for the last week.

I have to agree with @andreasabel here. I think _Preserves_⟶_ is a much more readable mnemonic than _[_]⇒_. To be honest I think I'd probably be much more in favour of deprecating _[_]⇒_ than adding _on[_]⇒_.

Sorry @m0davis I know that's probably not the answer you wanted.

[m0davis]

Actually, I'm perfectly happy with not adding _on[_]⇒_ so long as then _[_]⇒_ is deprecated. Would that mean (I hope) deprecating _Preserves_⟶_ as well?

[MatthewDaggitt]

Actually, I'm perfectly happy with not adding on[]⇒_ so long as then []⇒_ is deprecated.

Excellent.

Would that mean (I hope) deprecating Preserves_⟶ as well?

I think _Preserves_⟶_ still has a place as:

1. deprecating both would be removing existing functionality from the library which isn't ideal.

2. _Preserves_⟶_ is used in several places in the library (e.g. in the definition of congruence in Algebra.FunctionProperties), whereas I'm not aware of any uses of _[_]⇒_.

3. I think it's much more readable than _[_]⇒_. Personal opinion of course.

4. It has natural extensions such as _Preserves_⟶_⟶_

[laMudri]

Whatever is done here, it'd be nice if unary and binary relations had more consistent naming for their combinators. It's a bit annoying that predicates have _⊆_ where relations have _⇒_, and _⇒_ on predicates means something else.

[gallais]

@laMudri Have you considered using Relation.Nary?

[laMudri]

No. Is that module:

1. sufficiently populated with combinators?
2. usable where the existing combinators were used, in-place (via definitional equality)?

[gallais]

sufficiently populated with combinators?

I don't know what you need. Have a look

usable where the existing combinators were used, in-place (via definitional equality)?

Yes, expect for conflicting conventions naturally (it uses the same convention as
Relation.Unary).

[jamesmckinna]

Closing this: @laMudri 's point about consistency between Relation.Unary and Relation.Binary belongs as a separate issue? (Or even: gets rolled into #2091 ?)