Implement move-via-deprecate of `decToMaybe` as per #2330

[JacquesCarette]

Make the main home of decToMaybe be Relation.Nullary.Decidable.Core, but deprecate the one in Data.Maybe.Base instead of removing it entirely. Fix the library accordingly.

Note that this forces Relation.Nullary.Decidable.Core to use Agda.Builtin.Maybe to avoid a cyclic import. This can be fixed once the deprecation is done.

[jamesmckinna]

Needs a CHANGELOG! UPDATED: I took the liberty of adding one, and streamlining your deprecation en passant.

[JacquesCarette]

Indeed it does.

[jamesmckinna]

Also, is this an opportunity to follow through with @gallais 's suggestions following his comment on #2059 ? Given that once you've deprecated, you get to pick new/better names and change the API as well? or would you rather leave this to a subsequent PR? I think it would be a good idea... on whatever basis.

[JacquesCarette]

isTrue seems sensible.

[jamesmckinna]

My preference, now that it's under Decidable, would be #2059 's dec⇒weaklyDec... because all of those uses under Solver are about weakly deciding a property, but are written under the identification of that with Maybe...

... but isBlah is at least a conventional use. (Style guide again? Is it documented anywhere?)

I wonder if isTrue is a bit on the nose? (Potential conceptual clash with True connoting/denoting Bool in Decidable.Core?)

I'm really glad to be revisiting some of the choices under #2055 / #2058 / #2059 which I suspect got lost in the wash of the v2.0 release (and my mistake in tagging those as v3.0...), but it feels as though this more modest PR might be leaving downstream hostages to fortune if it chooses one particular new name. Sorry for suggesting it!

Perhaps, against myself, the thing is to stick with decToMaybe ahead of wider consideration of the naming issues. I feel genuinely conflicted between the minimum commitment solution and wanting to fix everything at once ;-)

[JacquesCarette]

Until I hear at least one more opinion, I'm going to leave it as decToMaybe. I do agree its name should change!

[JacquesCarette]

I'm fine with renaming it, and isYes is indeed not the best name either. But I must say that I hate dec⇒weaklyDec. The dec⇒ part is fine, it's the weaklyDec that I'm not happy with. What the heck is a "weak decision"? If this was long established vocabulary, sure. But I don't think that's the case. And 'weak' is ridiculously overloaded (and under-indicative).

In some ways justYes might be better (no, I'm not trying to pun here!) I would be fine with dec⇒justYes. I'm using 'just' in its 'truncate' sense here. I'm explicitly avoiding the term 'truncate' in the name, as this is a partial truncation, as that's a worse can of worms to open, IMHO.

[jamesmckinna]

I'd cheerfully take responsibility for the bad name, had I introduced it, but it seems to have been written into the library a long time ago... commit 5827d71af6f15bc3a3f8780c5659ee375e4c6639 part of v1.0!

I sympathise with whoever first chose "weakly" though: Johnstone in Topos Theory (1977) called 1+_ the "decidable partial map classifier" and there seems no easy way to extract a reasonable qualified adjective out of that, given that the other ready-at-hand prefixes "semi-" and "partial-" both connote the more established recursion theoretic 'yes definitely but may not terminate if no'... and recursion theory doesn't seem to have an agreed orthodox name for this useful middle ground?

But v3.0 as a holding pen for reconsiderations of this name, and v2.x for continuing with it for the time being?

That said, the writers of the various Solvers seemed (eventually) to bypass the issue entirely by working with Maybe directly, which is a different kind of (category) mistake IMHO (one of 'data vs. property'), so WeaklyDecidable has not really caught on.

I think for the sake of this PR, and its focus on simplifying dependencies, suggest sticking with the name, even if you hate it?

[jamesmckinna]

I took the liberty of resolving the merge conflict, but without committing one way or the other to my suggestions regarding qualified names above, and promptly screwed up the imports: the gap between Relation.Nullary.Decidable.Core exporting map′ and Relation.Nullary.Decidable exporting map has caught me out more than once :-( (and all for the sake of having a 'wrapped' or 'unwrapped' instance of Equivalence...)

[jamesmckinna]

Continues to look good! Can we get a second approval/review, please?

[MatthewDaggitt]

Meeting conclusion:

• Either change deprecation strategy to public re-export Nullary.Core name instead of redefining.
• Or rename Nullary.Core definition

[jamesmckinna]

Apologies! the last commit appears to have broken things, because Relation.Binary.Consequences, despite importing from the 'right' place, nevertheless triggers the deprecation warning... so should the v2.1 version not deprecate the name (I'd previously understood this as the intent of @MatthewDaggitt 's first suggestion, but then thought that the name could still be deprecated in Maybe.Base?) REVERTED

[JacquesCarette]

Implemented @MatthewDaggitt 's first deprecation strategy. This should be ready to go now.

[jamesmckinna]

So it seems as though the most recent commit from @JacquesCarette falls into the same trap as my (reverted) attempt: making the definition via public re-export seems to trigger the warning wherever the name is used, even if it is 'correctly' imported from Relation.Nullary.Decidable.Core (and not Data.Maybe.Base).

My reflections on/diagnosis of what went wrong for me (and hence here, too) is that @MatthewDaggitt 's first option requires additionally

• either waiting to deprecate the name until we agree on the new one
• or, adding a pragma to suppress the warnings in client modules

The second seems very undesirable for obvious reasons... and for the first, if we imagine changing the name downstream, then the old name decToMaybe will need to be deprecated in its new home Relation.Nullary.Decidable.Core (and whence, I think, the deprecation will also follow it to the old one Data.Maybe.Base), so I think the 'right' thing to do ahead of picking the right name is simply (!) to remove the deprecation warning from Data.Maybe.Base (and CHANGELOG) for the time being, until such time as the name is ready to be deprecated in Relation.Nullary.Decidable.Core...

... which feels a bit more painful in terms of delay, but better/cleaner in terms of workflow, until we can agree on the new name.

@MatthewDaggitt can you confirm this analysis?

[jamesmckinna]

I'm fine with isYes and isNo.

Originally posted by @JacquesCarette in https://github.com/agda/agda-stdlib/issues/2330#issuecomment-2154801919

On that basis, we could thus combine the rename with deprecation step in this PR?

[JacquesCarette]

Yes, that's my thinking.

[jamesmckinna]

Yes, that's my thinking.

Happy to push this if your hands are full!

[jamesmckinna]

Moved name discussion back to the issue... sigh.

[MatthewDaggitt]

Yes, as I said in the meeting, you can't directly attach deprecation warnings to re-exports. As @jamesmckinna suggests we'd have to remove the deprecation warning entirely and leave just a textual comment that it is deprecated. This is what we've done in the past in similar circumstances.

[jamesmckinna]

Looking at the details of this PR, much of the knock-on viscosity arising from any name change to decToMaybe could be dealt with by fixing the various DRY violations under Algebra.Solver.*Monoid, and by delegation from a given Relation.Binary.Definitions.DecidableEquality via Relation.Binary.Consequences.dec⇒weaklyDec... (and we can fix that name downstream... #2404 )

UPDATED: latest commits

• rename to dec⇒maybe
• deprecate in Relation.Nullary.Decidable.Core, with the fully-qualified name
• re-export publicly in Data.Maybe.Base for backwards compatibility, and to pick up the 'right' deprecation warning
• refactor the dependency on the new (provisional?) name via Relation.Binary.Consequences.dec⇒weaklyDec as a 'single' point-of-entry

Hope that's a good v2.1 solution, finally!?

[JacquesCarette]

Yes, this works. I'm fine with dec⇒maybe. Thanks.