[ deprecate ] `Relation.Nullary.Reflects` and [ refactor ] `Relation.Nullary.Decidable.Core`

[jamesmckinna]

Prolonged, and sustained, exposure to Relation.Nullary.Decidable{.Core} now leaves me thinking that the indirection via Relation.Nullary.Reflects is an unnecessary overhead, moreover one which complicates the deployment of the basic idea underlying @laMudri 's original refactoring, namely that a given a? : Dec A should be understood as, and manipulated as if, equivalent to if does a? then A else ¬ A. I would welcome discussion of this, given that I missed much of the archeology on this topic, but the (NB: breaking!) route map I have in mind goes something like:

0. breaking Refactor Relation.Nullary.Reflects to be a record, encapsulating the of/invert relationship:

record Reflects (A : Set a) (b : Bool) : Set a where
  constructor of
  field
    invert : if b then A else ¬ A

This would have the additional advantage of removing the cruft associated with ofʸ and ofⁿ, and hence of not being able to pattern match on the 'computed constructor' of (cf. Agda issue agda/agda#7061). Knock-on changes to the smart constructors for Reflecting the propositional connectives then involves a bit more explicit Bool case analysis, but that's already implicit in the use of the existing constructors...

1. Refactor Relation.Nullary.Decidable{.Core} to use the new definition (I've tried this, and the only change involves redefining the pattern synonyms yes/no to use of now instead of ofʸ and ofⁿ...)
2. Explore the knock-on consequences in the rest of the library: I conjecture none, given the care taken over several PRs to isolate the reflects abstraction: typically only invert is ever invoked (and occasionally of), to offer lazier versions of matching on yes/no.

A yet more radical departure would then be to observe that under 1. above, the indirection via Reflects/of/invert is now entirely redundant (and a potential time/space overhead; they are essentially no-ops, by eta, but the overhead of record marshalling/unmarshalling remains), but for, perhaps, considerations of laziness, and/or type inference when inferring A from a proof of Dec A (not sure about this...?)

So, I'm tempted to go further, and suggest:

1. [ alt ] Refactor Relation.Nullary.Decidable{.Core} to use the new streamlined definition (@JacquesCarette 's suggestions of verdict and rationale as alternative field names might now make sense, especially if we entertain this as a side-by-side alternative implementation for comparison with the existing implementation...)

record Decidable (A : Set a) : Set a where
  constructor _because_
  field
    does : Bool
    proof : if does then A else ¬ A

2. [ alt ] The knock-on consequences are now that of and invert disappear, and that we need to redefine the smart constructors for propositional decidability, avoiding the indirection via reflects, as follows:

T? : ∀ x → Dec (T x)
does (T? x) = x
proof (T? x) with x
... | true  = _
... | false = id

¬? : Dec A → Dec (¬ A)
does  (¬? a?) = not (does a?)
proof (¬? a?) with p ← proof a? | does a?
... | true  = _$ p
... | false = p

⊤-dec : Dec {a} ⊤
does  ⊤-dec = true
proof ⊤-dec = _

_×-dec_ : Dec A → Dec B → Dec (A × B)
does  (a? ×-dec b?) = does a? ∧ does b?
proof (a? ×-dec b?) with p ← proof a? | q ← proof b? | does a? | does b?
... | true  | true  = p , q
... | true  | false = q ∘ proj₂
... | false | _     = p ∘ proj₁

⊥-dec : Dec {a} ⊥
does  ⊥-dec  = false
proof ⊥-dec  = λ()

_⊎-dec_ : Dec A → Dec B → Dec (A ⊎ B)
does  (a? ⊎-dec b?) = does a? ∨ does b?
proof (a? ⊎-dec b?) with p ← proof a? | q ← proof b? | does a? | does b?
... | true  | _     = inj₁ p
... | false | true  = inj₂ q
... | false | false = p ¬-⊎ q

_→-dec_ : Dec A → Dec B → Dec (A → B)
does  (a? →-dec b?) = not (does a?) ∨ does b?
proof (a? →-dec b?) with p ← proof a? | q ← proof b? | does a? | does b?
... | true  | true  = const q
... | true  | false = q ∘ (_$ p)
... | false | _     = flip contradiction p

If I have understood the substance of the original rationale for the redesign, namely that does should be a cheap computation, but that if proof is actually required, then it may be expensive (and involve, inter alia, the hand-in-hand computation of does, thanks to the definitions of the smart constructors for Reflects...), then the above definitions don't fundamentally alter that state of affairs: the indirections via with would force the computation of does, while threading the recursive calls to proof exactly analogously to how these proceed at present. The only cogitive wrinkle is that the types of p and q change in each branch, according to the value of their associated Bool proxy does... much as we understand Dec as being supposed to behave!

It's entirely possible that this design has already been considered and rejected in the past, in which case I would welcome pointers to the relevant GH pages (or mailing list discussion etc.), but if not, I think that this could make for a very instructive redesign, even if, in the first instance, only a profiling experiment for side-by-side comparison with our existing implementation...

Comments welcome!