[ 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 https://github.com/agda/agda/issues/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!

[JacquesCarette]

I think the first refactor makes a lot of sense.

The second refactor scares me. Basically because of the indirection through with: this makes goals extremely hard to work with. If you know what you're doing, it is navigable (as you show in your code above), but during complex code development, these obligations might come from very deep inside the code and become quite baffling. It's not "wrong", in the sense that what is being asked for by the with is fundamentally required. It's the UX that is not so good. My feeling is that the UX of the first refactor will make more sense to users -- the record captures more of the intent.

[mietek]

Like I said in https://github.com/agda/agda-stdlib/pull/932#issuecomment-2939247172, I would still like to know if there is a measured performance benefit to rephrasing Dec in terms of a boolean and a separate proof, let alone more complicated constructs. The UX impact is real, and leads me to defining my own simple Dec in my own developments.

cc @laMudri

[jamesmckinna]

Thanks @mietek I think these concerns are orthogonal to the main argument in this issue, but indeed there's a general point that we don't have good performance comparison test rigs for evaluating this kind of large-scale design change...

... separately, I am also aware of your concerns about pattern synonyms vs. constructors, but again, I think that's orthogonal here (although I note in passing that one consequence of my more radical proposal is that yes and no seem to become more, not less, inevitable, although as they would also become mere abbreviations for true because and false because, we could consider some better constructor names in such a way as to avoid them altogether... such as reusing true and false themselves!?)

[mietek]

I agree; orthogonal. I think the yes and no problem should be fixed in the language itself:

• https://github.com/agda/agda/issues/7915

[laMudri]

Apologies for taking a while to get to this. I don't immediately see any problems with these two proposals, and if there aren't any hidden problems, then indeed both look better than what there is currently. Purely from memory, I imagine the reason for not using a record (as in the first proposal) is that I didn't understand the interaction with unification at the time, but somehow stumbled into the data type making things work more nicely. That said, I can't immediately come up with an example of where that unification behaviour is important, and whether such cases exist should decide between the two proposals given here. I have some vague memory that it maybe happened once or twice in the library, but in that case, one might well be able to argue that there's something else wrong with those examples.

It seems to me that the key unification case is Reflects ?A ?b ≟ ¬ B, where, if Reflects were an alias instead of a record/data type former, it would be unclear whether to solve it as ?A = B; ?b = false or ?A = ¬ B; ?b = true. With a record or data type, the constructor effectively delineates between the two sides of the equation. As I said in the previous paragraph, I can't remember how often you end up with this type of unification problem, which would arise from Reflects inhabitants/goals which are missing their Boolean value.

A minor disadvantage of the first proposal (with the record type) is that it requires one extra case split to reach the yes/no pattern synonyms. Currently, you can split on an x : Dec A and get y because z, and then split on z to get .true because ofʸ v and .false because ofⁿ w, which are automatically folded into yes v and no w (at least, if I remember correctly; I haven't tried it out). Under the first proposal, the quickest route is x ↦ y because z ↦ y because of u ↦ true because of u/false because of u, which fold into yes u/no u.

[jamesmckinna]

Thanks @laMudri for the feedback!