[ refactor ] name of Data.Product.Relation.Binary.Pointwise.NonDependent.×-decidable

[jamesmckinna]

Yet another item from #2846 .

NB. There's maybe an argument for saying that this should really consist of:

• rename Pointwise to _×_ (because this is 'merely' a lifting to Binary relations of the underlying Nullary combinator)
• rename ×-decidable to _×?_ (in some sense: ditto.)

UPDATED: now moved to DRAFT while we figure out the right solution to #2865

[JacquesCarette]

I agree with your really. Feels like this intermediate step is not needed, we should just go to the 'proper' names.

[Taneb]

If we rename Pointwise to _×_, how would we import the module qualified where we currently would have both Data.Product and Data.Product.Relation.Binary.Pointwise.NonDependent imported?

[gallais]

Should it be called All for uniformity?
That's what the pointwise lifting over inductive families is typically called.

[Taneb]

@gallais that's only so far for unary relations, right? This is far more analogous to Data.List.Relation.Binary.Pointwise for me (the notion of decidability for which is just called decidable!)

[jamesmckinna]

OK, thanks for piling in...

@Taneb regarding the choice of names, this is (was) intended to be one more chipping away at renaming X-decidable proofs to X?, so if Data.List.Relation.Binary.Pointwise needs to be updated, it always could be downstream (but if not, then as with #2955 I'm still torn as to whether this really is a good idea, so we should decide that first... on the issue perhaps!?)

@gallais your renaming suggestion for Pointwise makes sense to me, but then I find it hard to confidently arbitrate between the two heuristics:

• uniformity: there's a single name for this concept wherever it appears, as a... lifting of the container functor to predicates, relations... I guess is the intuition?
• name-fidelity: this is an arity-raising operation from Nullary to Binary (and then: why do we do it differently for Unary predicates?)

On the first suggestion, I guess that All/Any might be a way to go (but then I'd double down, and say why don't we use \box/\diamond instead?

I appreciate @JacquesCarette support for my suggestion, but I'd probably rather fix this up downstream, after we have had a 'proper' discussion on a separate issue?

UPDATED: no, let's just do this now.

[jamesmckinna]

As to how to import these things qualified, I'd be OK with

import ...Product.Base as Product using (...)
import ...Pointwise as Pointwise using (...)

and then distinguishing Product._×_ from Pointwise._×_?

UPDATED: or else, as on master now in certain modules, with a renaming (_×_ to _×ᴿ_) directive on imports of Pointwise...

[jamesmckinna]

Aaaargh/A-ha: in Data.Product.Base, we already have, at too specialised a type to capture Pointwise, but nevertheless an instance of the construction:

_-×-_ : (A → B → Set p) → (A → B → Set q) → (A → B → Set _)
f -×- g = f -⟪ _×_ ⟫- g

Should we also consider deprecating this? Or generalising it and using this name instead?

NB this definition is (essentially) the pullback of _×_ along the diagonal maps for A and B, so might be refactorable via On... another time perhaps!

[JacquesCarette]

Aaaargh/A-ha: in Data.Product.Base, we already have, at too specialised a type to capture Pointwise, but nevertheless an instance of the construction:

_-×-_ : (A → B → Set p) → (A → B → Set q) → (A → B → Set _)
f -×- g = f -⟪ _×_ ⟫- g

Should we also consider deprecating this? Or generalising it and using this name instead?

NB this definition is (essentially) the pullback of _×_ along the diagonal maps for A and B, so might be refactorable via On... another time perhaps!

What generalization do you have in mind? (Definitely should be done in a different PR).

[jamesmckinna]

Aaaargh/A-ha: in Data.Product.Base, we already have, at too specialised a type to capture Pointwise, but nevertheless an instance of the construction:

_-×-_ : (A → B → Set p) → (A → B → Set q) → (A → B → Set _)
f -×- g = f -⟪ _×_ ⟫- g

Should we also consider deprecating this? Or generalising it and using this name instead?
NB this definition is (essentially) the pullback of _×_ along the diagonal maps for A and B, so might be refactorable via On... another time perhaps!

What generalization do you have in mind? (Definitely should be done in a different PR).

It may be easier to write and typecheck than to try to explain... ;-)

But we do have a function in Function.Base:

_-⟨_⟩-_ : (A → C) → (C → D → E) → (B → D) → (A → B → E)

which would then be applied at A → A × A and B → B × B to A × A → B × B → Set _ given by L × R for... oh L and R are then... also more complicated by being on proj for the relevant projections ugh. Worse than I thought, even though it seemed 'obvious' to me when I wrote the previous comment. One for the obsessives only, I suspect.

[MatthewDaggitt]

I'm not sure about this at all. Agree with @Taneb that we probably don't want to conflate the type combinator and the relation combinator.