agda-stdlib move `decToMaybe` from `Data.Maybe.Base` to `Data.Maybe`

decToMaybe drags in Relation.Nullary.Reflects and Relation.Nullary.Decidable.Core (which is a reasonable thing to do for its definition). But this seems like "overkill" for a .Base module as 'core' as for Maybe.

The fixes to the library are trivial - no code expects it to be that low. This, in theory, should not affect external code either, as people shouldn't be digging into .Base modules. But this would still be an (extremely minor) breaking change. Is that allowed for 2.1? Frankly, I don't think anyone would notice!

Mar 27 '24 02:03 JacquesCarette

Base modules are part of the public API. Core modules are not. So yes this would be a breaking change by our published policy, so adding this to the version 3.0 milestone.

Mar 27 '24 02:03 MatthewDaggitt

As discussed between me and @gallais on one of my many Relation.Nullary PRs #2059 I think that decToMaybe belongs under Decidable, and not under Maybe. So probably even more so a v3.0 change, but then we could get to rename it, too...

Mar 27 '24 08:03 jamesmckinna

If we could come up with some kind of rule of thumb for where these things belong? I'm fine with this moving to Decidable, BTW.

Some kind of (ad hoc) ordering on concepts?

That might, for example, let us move the functions relating Maybe and These to somewhere else. It's not causing a lot of headaches, but it seems like a small wart indicative of the larger issue.

Mar 27 '24 11:03 JacquesCarette

So, for me at least, the ordering is induced by information loss/ornamentation/dependency:

Reflects and Decidable are a 'richer'/'better' Bool, so functions to Bool belong under Reflects/Decidable etc.
ditto. for Maybe, especially if we go via WeaklyDecidable
properties/Preds are 'richer' than their underlying Data, so toData functions belong under the Pred definition
etc.

Is that a plausible heuristic?

TL;DR: toX is/should (always?) be regarded as a forgetful (homo) morphism?

to erases... from reinscribes structure eg a List gets its length as a decoration/ornamentation when passing 'from' List to Vec...

Mar 27 '24 11:03 jamesmckinna

Rather than make the proposed breaking change, why not start more conservatively, with:

deprecating the function in Base for v2.1, in favour of a definition in Decidable
make the breaking change in v3.0

(Trying to channel my inner @MatthewDaggitt on this one ;-))

Mar 29 '24 06:03 jamesmckinna

I tend to not think of such sensible changes because it doesn't actually fix what I see as the real problem (i.e. the bad dependency). But it is a good idea.

Also: we should have the "rule of thumb" discussion in its own issue, it's going to get lost buried in here.

Mar 29 '24 20:03 JacquesCarette

See PR #2336 for the implementation of @jamesmckinna 's suggestion.

Mar 29 '24 21:03 JacquesCarette

It's not breaking, it is merely deprecation. Especially once it gets a new name, then it won't cause spurious clashes.

Mar 31 '24 13:03 JacquesCarette

@gallais suggested isYes and isNo on #2059 for the two operations decToMaybe and the one which currently has no name (and no definition ;-)).

If we agree on those now, we can 'upgrade' #2336 to reflect this analysis...?

Jun 07 '24 11:06 jamesmckinna

I'm fine with isYes and isNo.

Jun 07 '24 13:06 JacquesCarette

Suggest updating the milestone to v2.1, and adding decToMaybe to the list of deprecations to tidy up/remove in v3.0?

Jun 07 '24 13:06 jamesmckinna

Agreed, i.e. I can commit to that.

Jun 07 '24 13:06 JacquesCarette

I'm fine with isYes and isNo.

Aaargh! Wasn't thinking when I took @gallais 's suggestion...

... isYes is the name of the projection from Dec to Bool %!$#

What about decYes and decNo? (both terrible, but what can we do...)

Jun 07 '24 17:06 jamesmckinna

Suggestions: isYes? and isNo? (i.e. with the ?) yes? and no? . There might be other 'signs' of decidability also used in the library?

I'm not entirely against decYes and decNo but they are terrible, so it's worth thinking some more before settling.

Jun 07 '24 18:06 JacquesCarette

I'm coming round to your original suggestion (contra dec⇒weaklyDec) of justYes (and hence justNo)... unless we go the whole way with isJustYes and isJustNo? The problem with the isX idiomatic usage is that in this situation, the constructor name X alone is/seems insufficient to connote what's happening in the type...?

Jun 08 '24 03:06 jamesmckinna

Against my last comment, I'll suggest instead the 'purely cosmetic' dec⇒maybe, which at least permits:

the deprecation to be recorded in v2.1
PR #2336 to be left in a consistent state
alleviates @MatthewDaggitt 's concern about name clashes arising from simultaneously opening each of Data.Maybe.base and Relation.Nullary.Decidable.Core
the question of naming (and eventual removal of the deprecated name) to be punted to v2.2 and beyond... or sooner if we can get our act together ;-)

Is that reasonable?

Jun 08 '24 09:06 jamesmckinna

I'm torn. Now that I've seen that there really ought to be two functions here, not just one, it's kind of hard to go with dec⇒maybe. Which speaks in favour of justYes and justNo. But also getting this done for v2.1 is definitely appealing, and if that means dec⇒maybe then so be it!

Jun 08 '24 12:06 JacquesCarette

I'm torn. Now that I've seen that there really ought to be two functions here, not just one, it's kind of hard to go with dec⇒maybe. Which speaks in favour of justYes and justNo. But also getting this done for v2.1 is definitely appealing, and if that means dec⇒maybe then so be it!

Re: the second operation. As it's easily expressible as a composition of dec⇒maybe and ¬?, it (perhaps) doesn't need a life of its own?

Re: a v2.1 solution: see most recent commits on #2336

Jun 09 '24 08:06 jamesmckinna

Thanks!

Jun 09 '24 11:06 JacquesCarette