dependencies of things (vol. 94): `Relation.Nullary.Decidable`

[jamesmckinna]

Working on PR #2055 drew my attention to the following dependency design 'indecision', probably arising from previous large-scale refactorings:

• Relation.Nullary.Decidable imports Data.Sum.Base but does not use it at all (anymore) UPDATED this non-dependency now seems to have been fixed
• Data.Sum imports various ('the usual') things from Relation.Nullary.*, but all/only in the service of defining

-- Conversion back and forth with Dec

fromDec : Dec A → A ⊎ ¬ A
fromDec ( true because  [p]) = inj₁ (invert  [p])
fromDec (false because [¬p]) = inj₂ (invert [¬p])

toDec : A ⊎ ¬ A → Dec A
toDec (inj₁ p)  = yes p
toDec (inj₂ ¬p) = no ¬p

So a question naturally arises (usual asymmetry between which module in a to*/from* scenario takes ownership of the functions) whether

• (NOCHANGE) Data.Sum should continue to import the relevant pieces of Relation.Nullary.*
• (CHANGE) else Relation.Nullary.Decidable (NOT or .Core? not sure about the potential dependency cycles here) should continue to import Data.Sum.Base, but also define fromDec and toDec, drastically simplifying the import list for Data.Sum

PROPOSAL: adopt the second 'CHANGE' option, on the basis that Sum is conceptually/computationally prior to Decidable (so should have 'lighter' dependencies), moreover these functions only exercise specialised instances of _⊎_

A followup question would/might then be, cf. #2058 :

• possible candidate renamings of these functions

fromDec ↦  dec⁻
toDec ↦  dec⁺

• or else

fromDec ↦  toSum
toDec ↦  fromSum

[jamesmckinna]

Similarly Data.Maybe.Base.decToMaybe?

[gallais]

isYes : Dec A → Maybe A
isNo : Dec A → Maybe (¬ A)

?

[jamesmckinna]

Sorry to be obtuse, but not sure what your point is here @gallais ? Can you explain for the sclerotic-brained?

[jamesmckinna]

And in the interests of full disclosure, my 'point', as such, is to register surprise that Maybe.Base imports Decidable.Core, when it is already the case that Decidable imports a bunch of Data.* type constructors (but not Maybe, for some reason?), so 'it makes sense' to localise the interaction between Dec/Decidable and Maybe to the Relation.Nullary.Decidable.* subtree, rather than burden Maybe with it. Esp. Base... there seems nothing about this which is 'basic'!

As with Data.Sum, there seems to be a (creative? useful?) tension between Dec as a property of types, and as some sort of 'type constructor'. But I guess it sits better with me to accent/refactor towards the former, not the latter...?