Snoclists?

[gallais]

Snoclists (lists that grow on the right rather than the left) are commonly used when
representing syntaxes with binding because they grow the same way contexts grow
which allows you to transcribe everything without having to "think backwards".

They're also really useful to represent the intermediate state of a computation slowly
going through a list left-to-right with the "fish" combinator having elements in the
middle freely flow from one side of the divide to the other without the need to deploy
rewrite rules (which you would need if you were using a pair of lists instead).

Are we open to adding them to the stdlib (I'm finally open this up because I need them
for the nth time and they're not available)? They're part of Idris 2's prelude for instance.

• Snoclist lib
• Port of scoped reflection API: https://github.com/agda/agda/blob/4f31b6962af225711e70b26dc905b7517e38d0de/notes/reflection/ReflectionWellScopedList.agda

[JacquesCarette]

Strong YES from me.

Not only is your reasoning sound, one can also witness that Agda is used a lot by people doing PL meta-theory. We should strive to make their lives easier.

[Taneb]

Can this be implemented as pattern synonyms on List, so we don't need to reimplement all the functionality?

[jamesmckinna]

Yes from me as well.

To @Taneb , at least from my memory of trying this the last time I refactored the Data.List.Base.InitLast section, no it can't be done with pattern synonyms, without (re)evaluating the whole list in your hand, as it were.

To @gallais given the intimate intertwining of the two datatypes, does it make sense to have them both defined, in Data.List.Base, or can the dependencies be unwound so as to make a clean separation into two modules, with 'snoc' importing 'cons'?

And: naming... will we be able to agree on names for all the gadgets? Eg. reusing _∷ʳ′_ (ugh! the choice of this name for the constructor, and _∷ʳ_ for the 'snoc' operation on List... is perhaps unfortunate)

Ob: names. We have Data.List.Base.InitLast, but Data.List.NonEmpty.Base.SnocView!?

[gallais]

Pattern synonyms don't lead to cleaner goals which is the point of this.

[JacquesCarette]

Sigh - another case where metaprogramming would probably be a reasonable solution.

I've been having many discussions (with @TOTBWF ) about how I think we ought to be able to inform our ITPs about even more of our intentional information (yes, with a 't' here, but I'll live with being able to be more intensional if that's all I can get).

[TOTBWF]

STRONG +1 on this: we've been using https://opam.ocaml.org/packages/bwd/ in RedPRL projects for years and it makes life so much easier.

[gallais]

I just had my last lecture for this (academic) year earlier today so should have a bit
of time reasonably soon-ish to take this on :)

[jamesmckinna]

Comment on the reflected syntax, ahead of any PR: why distinguish constructor [<] from []?
Overloading constructor names is a feature/virtue, not a bug...

Similarly/but more controversially, I'd like/would prefer to be able to overload the 'cons-right' symbol of Data.List.Base etc., but that may be a stretch too far, and offend against established fish-based canons... ditto 'append-right' etc.

[gallais]

I think we absolutely need to break the symmetry for the cons/snoc. I am happy to
revert the cosmetic distinction between [<] and [>].

As for the cons-right symbol, I'm afraid it's just not possible because Agda refuses
to do type-directed disambiguation as soon as functions are involved.