Ergonomics of trying to add 'constructors' in Data.Vec.Functional.Relation.Binary.Pointwise.Properties

[jamesmckinna]

So the issue title is a huge mouthful (and the text of this issue; -- sorry!), but the issue falls into two parts:

• (general) ergonomics of 'pseudo' constructors/introduction forms for not-necessarily inductively-defined concepts;
• (specific) in the particular instance of Data.Vec.Functional.Relation.Binary.Pointwise{.Properties}

I'll use the second to illustrate the first (see branch vec-functional on my fork; it seems to be the easiest way to flesh out the issue):

• Data.Vec.Functional.Relation.Binary.Pointwise defines a relation transformer Pointwise, defined on R : REL A B ℓ, All-style as a function returning instances of R for each index i of a functional representation of Vectors over A (resp. B);
• such a relation, morally at least, has two 'pseudo-constructors' (introduction forms) for the [] and _∷_ cases
  BUT
• while concretely instantiating Pointwise at a given R is OK;
• it seems hard to associate the corresponding instances of the pseudo-constructors as, as it were, 'constructors' of that given instance of Pointwise R

So...

• there's a 'coupling' issue: the typechecker isn't smart enough to infer the relevant R when appealing to the constructors;
• I've ended up having to create a specific submodule Constructors of ...Properties which declares them, explicitly parametrised on R (see branch), and then opening an instance of that at the same time as defining a Pointwise instance

I've created a branch (towards a PR?), and example uses of it (not shown), but the 'issue' for me is two-fold:

• is there (not?) an easier way to do this?
• does this pattern (pseudo-constructors for recursively/non-inductively defined notions) arise in other settings, and if so, how have other people tackled it? (In other work with @gallais , we've wrapped the functional representation inside a record to overcome the limitations of the typechecker, but is that the only way to deal with this? EDITED: also cf. Data/Vec/Relation/Binary/Pointwise/Extensional)

The other side of the 'issue' is that it seems (to me at least) that when stdlib introduces new concepts, it should also provide appropriate introduction/elimination forms, as in the Constructors module. This is 'easy' for inductively-defined concepts, the constructors (or pattern synonyms on top of them) do the work; but this is an instance where they both seem useful/systematic to add, but are nonetheless absent.

(Similar consideration apply, more easily, to ...Relation.Unary.All cases for [] and _∷_)

[MatthewDaggitt]

Sorry for taking so long to reply to this!

I have also on occasion run into similar problems! In the end I always found that if I needed to inductively extend the vectors or their proofs then I should really been using Data.Vec rather than Data.Vec.Functional. In practice Data.Vec.Functional is really only designed to be used for fixed size vectors.

I'm unsure what you and @gallais are doing, but are you sure Data.Vec.Functional is the right tool to use?

[MatthewDaggitt]

Unusually this is actually documented 😆

agda-stdlib/src/Data/Vec/Functional.agda

Lines 7 to 12 in 6630bd9

	-- This implementation is designed for reasoning about fixed-size
	-- vectors where ease of retrieval of elements is prioritised.
	-- See `Data.Vec` for an alternative implementation using inductive
	-- data-types, which is more suitable for reasoning about vectors that
	-- will grow or shrink in size.

[jamesmckinna]

So, a couple of things things in play:

• the earlier work with @gallais (jww McBride, Chapman, Atkey) revolved around using a functional representation of environments in considering (instances of, and a generic framework for) 'environment-based' models of languages with binding;
• the 'fixed size' question (more generally), and the significance of the comment, which I had not really appreciated up until now;
• the (perhaps) yet more general issue of providing suitable 'constructors' for functional representations, in any case, and how to manage the type-checking/inference problems to which Agda is then susceptible.

The first, viz the use of a functional representation, there was to profit from an observation of Alan Jeffrey to the effect that, 'function composition is easier than...' well, most things, actually (cf. lists vs. difference lists). The solution we adopted was akin to that in Data/Vec/Relation/Binary/Pointwise/Extensional, namely to wrap the function inside a record, and do some fairly deft 'smart constructor' style manipulation to manage the marshalling/unmarshalling from the record.

The application I had been working on is a variation on that theme, namely a streamlined proof of the logical relations-style argument about CBN simulating CBV. So it's not that I need a Vector-based presentation per se... simply that it was convenient, seemingly cheap, but nevertheless required suitable Pointwise extension of certain relations from values to environments... and then I found myself needing 'constructors'.

So indeed, perhaps the correct answer is to rewrite in terms of a Vec-based representation. I'm grateful for the steer in that direction

Regarding the second and third points: the second, duly noted; the third, perhaps, remains moot.

I'll play around with the alternative, and presuming it all goes smoothly, abandon the issue (and the branch I had been developing towards a PR...)

[jamesmckinna]

Resolved with very little fuss. The only wrinkle seems to be agda's concern about ambiguity between Data.Vec.Base.lookup and Data.Vec.Relation.Binary.Pointwise.Inductive.lookup which it doesn't seem able to disambiguate by type... but otherwise I'm happy to close the issue.

[gallais]

I don't know about fixed size, @laMudri's original motivation to use Fin n -> a rather than
Vec n a was that (together with a better definition of decidable equality) big operators like
sum would be better behaved. The need to combine/extend functional vectors naturally
arises when merging sums.

I think the Relation.Binary.Pointwise design may have arisen has an overcorrection to the
Data.Table design mistake (#870). You do not need a record wrapper to reconstruct A from
Fin n -> A but you do need one for Relation.Binary.Pointwise because you cannot in
general reconstruct R from (i : Fin n) -> R (f i) (g i).

[jamesmckinna]

OK @gallais thanks very much for re-opening this, and for the pointers back into the history of stdlib and Data.Vec.Functional.

I was aware of the ++⁺ style constructors, for relations over each Vectors and Vectors, so in a sense I was wondering about the simpler corresponding instances for [] and _∷_ ... and noting their absence.

I was also aware (and perhaps complaining about) the need to finesse the typechecker into correctly inferring the associated R from an instance of Pointwise R... it's clear that in general one can't expect unique solutions (or any) to the corresponding higher-order unification problems (but there might be opportunities to heuristically guide that search?) so your comment about it perhaps being an overcorrection is... interesting.

For the intended modes of use (big Operators) how much performance overhead might one expect if Relation.Binary.Pointwise were to be re-implemented with a record wrapper, if I understand that to be your hint. Is this an experiment worth doing?

As to that intended mode of use, the examples in the library seem to revolve around n-ary summation in Monoid... written as a vanilla foldr. It's noticeable that the various *.TCOptimised implementations of addition and multiplication take care to account for the 0-ary and 1-ary cases specially... should this not also be the case for the big Op implementation in terms of Vectors?

[laMudri]

I haven't carefully read the above discussion, but maybe I have something relevant to add (now I've been summoned).

Subsequent to working on the Data.Vec.Functional hierarchy, I've found that whenever I want to prove some sort of Pointwise R (x ∷ xs) (y ∷ ys), the lemma I actually need is (modulo some implicit variables and generality of element types):

_∷₂_ : {xxs yys : Vector A (suc n)} → R (head xxs) (head yys) → Pointwise R (tail xxs) (tail yys) → Pointwise R xxs yys

The idea is to turn a green-green unification problem into green-purple problem (for the real constructors of inductively defined Vec, the problem was red-red rather than green-green, which is why the first thing you thought of would just work). Note that head (x ∷ xs) = x and tail (x ∷ xs) = xs judgementally (thanks to η for functions), so we get the expected goal types for the arguments to _∷₂_.

Occasionally the green and purple are the other way round, because we're synthesising the parameters x ∷ xs and y ∷ ys rather than checking against them. For those cases, I keep around a _∷₂′_ with the more obvious/naïve type, whose definition is just _∷₂′_ = _∷₂_.

[jamesmckinna]

Hmmm... wow!? regarding a much more sophisticated collection of insights than I was quite expecting (what did I expect, really?).
Much food for thought... thanks!? (oh, and separately/offline, given that I can't remember all the colour semantics, can you remind me what 'green-green' and 'green-purple' are supposed to mean in this context... and 'red-red' for that matter? I'm sure it's obvious, but it's simply not part of my tacit knowledge)

[gallais]

In Collie (declarative hierarchical command line interface library for Idris2) we have a similar story because we
found that we needed two kinds of smart constructors depending on whether we expected the type of the result
to be known vs. we wanted it to be inferred from the user-written expression.

https://github.com/ohad/collie/blob/main/src/Data/Record/SmartConstructors.idr for the curious (the important
things are the types of the two (::): in one case the index in the return type is extended with the newly added
entry, in the other there's a computation in the index of the type of the premise that removes the entry that was
just covered).

• green = traffic light says go = things that compute
• red = traffic light says wait = constructors

I don't know what purple is but I'm assuming it's a mixture of green & red (e.g. record projections because eta means we can solve more green-looking stuff?)

[jamesmckinna]

Again: great to have the additional (rich; expert) insights from other settings, and in particular the need/utility of smart constructors... but with the additional twist of the infer/check distinction.

Plus, I've seen references to collie before, nice to find out (a glimpse of) what's going on there...

[laMudri]

Purple is variables.

[jamesmckinna]

I'd be happy to close this 'issue' now, but grateful in the meantime for all that it has helped teach me about (some of the agda/agda-stdlib) library-design philosophy. Thanks!