Naming inversion principles for (one-constructor) `data`types

[jamesmckinna]

Inversion (in Prawitz' sense) of inductive definitions is a special case of pattern-matching, corresponding to there being a unique combination of premises for an inference rule which guarantee the form of the conclusion, namely those given by the premises of the rule itself. Cf. irrefutable with... which corresponds to a given instance of an inductive family having a 'constructor' which gives rise to the instance. A further special case occurs when we have a data type with only a single constructor, which somehow captures that scenario for all such instances, uniformly.

In the library, there are many examples of such phenomena, but all with ad hoc names, eg:

• [ ] in Induction.WellFounded, we have acc-inverse as the inverse of the single constructor acc (sic);
• [ ] in Data.Rational{.Unnormalised}.Properties we have drop-... as the corresponding inversion principles for the various equality/ordering relations, to strip off the unique associated constructor, in order to expose the underlying (typically Integer-based) relation instance;
• [ ] in Data.Nat.Base, we have, since #2000 , the inversions s≤s⁻¹ and s<s⁻¹ for the (obvious) instances of the associated type families _≤_ and _<_;
• [ ] in Relation.Nullary.Reflects, we have invert as the inverse of of, where the implicit Boolean argument ensures that we have 'unique' inversion; and there are probably several/many more to be unearthed.

PROPOSAL: that we agree on a consistent naming scheme for such things, add it to the style guide, and refactor/deprecate existing definitions in order to exploit it. Naturally, I would argue for ⁻¹ as the 'minimal-ink' uniform suffix for such names, thus:

• [ ] acc-inverse $\mapsto$ acc⁻¹
• [ ] drop-*≤* $\mapsto$ *≤*⁻¹ etc.
• [ ] invert $\mapsto$ of⁻¹ (this is already part of #2149 , but I would also recommend choosing a better root name than of here) etc. And to do so as soon as practicable, so that further incoherent/non-uniform choices do not get added elsewhere.

[JacquesCarette]

I'm completely for consistency. And your reasoning is great.

And yet, I'm not sure I really like ⁻¹ as the solution. Basically I think it boils down to 'inversion' being too overloaded a concept, with ⁻¹ being even more overloaded. In other words, while this solution is great for experts who already understand your reasoning above, it could be quite mystifying to all others.

For some odd reason, I got used to the Haskell-ish un prefix. I don't really think this is a particularly viable alternative, but I figured I would mention it, in the spirit of furthering discussion.

[jamesmckinna]

Re: haskell un: I have always considered that one of the many barbarisms/abominations given to the world (but it pales next to the type-constructor-name/value-constructor-name punning...) for which I always preferred capital case for the (newtype) constructor, and lower case for its 'inverse', by analogy with Maybe/maybe that we have in stdlib, again FWIW... Re: ⁻¹ I think above all I wanted something that was minimal-/minimum-ink. Questions of (avoiding) Unicode aside, I couldn't think of anything comparably 'lightweight'. Agree the (semantic) overloading might be an issue, but I think that might be overcome by also being systematic about proving that these operations (up to suitable Setoid equalities if need be) are actually mutually inverse...?