Naming inversion principles for (one-constructor) datatypes

[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 Refactoring (inversion) properties of _<_ on Nat, plus consequences #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 Enhancement to Relation.Nullary.Reflects etc. #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...?

[jamesmckinna]

@JacquesCarette did you ever think up a better alternative to ⁻¹ than un? It seems a small hill to die on, given that we agreed in principle above to (try to) enforce uniformity as both principle and practice, but I'm not sure I quite have the energy to pursue this until we have agreement, rather than present a fait accompli PR... or would that be the required forcing function to achieve consensus?

[JacquesCarette]

Coming up with a better one would have required actively thinking about it... which I'm only able to now.

Let me "think out loud" here. I tend to conceptualize removing the tag/constructor of a one-constructor data type as 'untagging' rather than in terms of inversion. More generally, I see a data type (i.e. sums-of-products) as being a means to partition a space (type) into pieces where knowing which 'piece' you are in gives you more information.

It is not wrong to see the act of removing the (useless) tag as some kind of inversion, as you are un-doing the act of tagging, i.e. inverting that tagging operation. But given just how many kinds of inverses there are, conceptualizing this one differently is most likely useful!

Weirdly, that seems to argue for un. Which I'm still not advocating! I guess some flavour of down-arrow would be just as evil?

Googling around, 'untag' can also be called 'strip', 'drop' and 'unlabel'. There's also 'detag' - but yuck! on that one. Apparently 'ostracize' is seen as somehow being related to 'untag' ? Hmm, doesn't seem like fertile ground (except for bad jokes) down that alley!

Hmm, what about riffing on 'set minus' and using a leading backslash? Removing foo might even be done as _\foo as a postfix operator. [I must admit I rather like that idea.]

[jamesmckinna]

Lots of food for thought!

After a few days' post-Christmas (in)digestion, however, I still find myself unconvinced by the arguments in favour of the alternatives you offer... although I have in the past when teaching Knaster-Tarski etc. referred to the ϕ X ⊆ X closure property as 'admits constructors according to ϕ', and the X ⊆ ϕ X consistency property as 'admits case analysis according to ϕ' rather than try to name those arrows according to some h/h⁻¹ convention nor their 'post'/'pre' fixedpoint nomencature, as there doesn't seem to be a standard convention for that, either!), but... intuition. FP convention, following Plotkin's FPC and others, seems to have in/out, fold/unfold etc. pairs of ASCII names for these things, but... Unicode lets us go beyond that, and the hobgoblin of my small mind is after consistency first, and minimum ink, second. The hard work is in choosing the constructor name... although given that we can overload those, maybe we should do that too!

I suppose, notwithstanding that you don't like the suggestion, that conversely, I had been thinking about ⁻¹ precisely because Lambek's lemma observes that the initial (resp. final) algebra (resp. coalgebra) map corresponding to the intuitive 'tagging' operation is invertible (notwithstanding any other fine words about proof-theoretic inversion). Elsewhere, we do of course use the ⁺/⁻ suffixing convention for intro/elim pairs for operations wrt predicates/relations, and I suppose I also wanted something which went with, but ever-so-slightly distinct from, that convention...

[JacquesCarette]

Feels like we need a third voice (or more) in here. We most certainly agree on the semantics of what we're talking about. We just disagree on what syntax to (ab)use.

[MatthewDaggitt]

I'm afraid I don't have a strong opinion on this. I'm happy with ⁻¹. Coming up with an entirely new scheme has the disadvantage that we'd have to rename everything, whereas with ⁻¹ we'd only have to rename some.

[JacquesCarette]

What do @Taneb and @gallais think?

[gallais]

I don't have a strong opinion