move `decToMaybe` from `Data.Maybe.Base` to `Data.Maybe`

[JacquesCarette]

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!

[MatthewDaggitt]

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.

[jamesmckinna]

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...

[JacquesCarette]

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.

[jamesmckinna]

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...

[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 ;-))

[JacquesCarette]

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.

[JacquesCarette]

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

[JacquesCarette]

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

[jamesmckinna]

@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...?