[discussion] a view-based analysis of punchOut, punchIn and pinch from Data.Fin

[jamesmckinna]

Currently lodged in Data.Fin.Relation.Ternary, but if I were to add more of these (see also PR #1901), I'd be strongly tempted to have a separate category, rather than something (of potentially arbitrary arity) under Relation.*... I'd suggest under View.*. Thoughts welcome.

This is an obvious duplicate/competitor to PR #1913 but founded on a slightly different basis.

No CHANGELOG at this stage: for discussion only.

[JacquesCarette]

Would it be possible to have a little bit more documentation above View in all three files? I can almost reconstruct what it's supposed to mean, but I'm not sure I could 6 months from now. As far as I can tell, this seems like it could be quite useful for doing things that are Fin-indexed and one wants a view of them that focuses on a particular index.

[jamesmckinna]

OK, thanks for this Jacques. Views such as these really are the inductive definition of the 'graph relation' of the function concerned: each constructor corresponds to a particular call-pattern in the original function definition; recursive calls are represented by inductive premises etc. And the recursion/pattern analysis of the original function definition (which is responsible for showing termination in the first place) is then exactly replicated in the definition of the covering function view ... so I'll try to distil the above words into the module commentary.

As to their possible use, as with PR #1923, it's really a case of wanting to contrast an ostensibly ad hoc analysis as in PR #1913 with a systematic derivation of the same properties by dint of... 'programming from the specification'. The original functions themselves were introduced by Conor in his paper on unification by structural recursion (they're context manipulations to insert/delete new (meta)variable positions, IIRC), and I guess that Nathan is using them in his ongoing work on permutations on Fin n via transposition lists.

... and yes, it seems valuable to insist that each relation always be called View, and the covering function view etc., because these are bits of gadgetry induced automagically by the original function definition... but I have always been too faint-hearted to try to implement the general scheme using Reflection...

[Taneb]

I'm afraid to say that to me this seems like an awful lot of machinery to produce proofs that, in this case at least, are not significantly more understandable

[jamesmckinna]

Nathan, thanks for that. While I am tempted (from one side) to agree, from the other I am/have been trying to argue that for subsequent properties that you may wish to have about these functions (your examples of preserving and reflecting orderings are just that, examples), having a general method might be preferable to having to rethink a pattern analysis each time.

Your PR #1913 is admirably clear, and even draws attention to the need for "better patterns"; the method of views-of-functions provides a way to encapsulate such 'better' choices once and for all. Eg your proofs for punchOut require different pattern analyses for the -mono and -cancel cases; in the view approach, not so.

I started to think about this (and the related PR #1923 ) after reading your proofs and those of @uzytkownik regarding lower₁ and inject₁, and finding myself irked (perhaps more than that) by all the clutter associated with repeated fiddly low-level reasoning about the n≢i domain side conditions. The View/view approach, once again, encapsulates that once and for all, and provides additional (redundant) recoding of those pre/post conditions as part of the general picture.

So yes: more weight, but I would argue, more power, and with it more reusability downstream.
UPDATED: extensive refactoring along the lines of PR #1923 together with READMEs giving the proofs of all the (corresponding) properties in Data.Fin.Properties, including the showstopper that punchIn and punchOut are (appropriately) mutual inverses, because their corresponding Views are converses (and no reasoning with the domain predicates required, because these are inductive invariants of the Views)

[jamesmckinna]

I'm going to close this for now, against a future version of the library which might make more use of views/view-based programming.