Association lists and their functions

[Saransh-cpp]

I am currently looking to port lookup, lookupBy, insertAt, and deleteAt from Idris2, but I am not sure if they are exactly required in Agda. It does look like that they do not exist in Agda. If they should be added in, should the API of lookup and lookupBy stay the same, or should it be changed (given that I could not find any such pair of functions in Agda)? Thanks!

[jamesmckinna]

deleteAt appears to be the _─_ operation?

No answer to why there isn't (?) the companion insertAt (though there are insert and remove in Data.Vec.* etc. I think ... this may be yet another knock-on consequence of List and Vec not being mutually consistent, so a separate issue/PR might be to tidy up both so that they are consistent, to the extent to which that's possible? It's certainly come up for me before...)

As for association lists themselves, I'd be tempted to organise them under Data.List.Association.* rather than try to shoehorn them into Data.List.Base? They're a distinguished mode of use of lists, satisfying the finite Map API, and that little theory seems worth abstracting out on its own? Just my opinion, though!

[jamesmckinna]

As to the question about API design, as a precursor to eventual implementation, should we consider more deliberately discussing those as separate issues/PRs/threads on the Zulip (under the #stdlib channel?) UPDATED see also my comment on #1911

[jamesmckinna]

And now returning to the main question: how much of idris2's (or that of any classical/orthodox Boolean-valued/simply-typed approach) behaviour on association lists can be realised in terms of the Data.List.Relation.Unary.Any machinery, suitably specialised? Question prompted by threading back through the definitions in Data.List.Membership etc. ...

... so if it does turn out to be possible to 'encode everything' that way, that doesn't stop it being independently interesting to consider versions specialised to lists of pairs, where the 'unary' predicate on pairs is induced by ... a binary, Boolean-valued function. Not least because, from a pragmatic point of view, for the hypothetical 'haskell-inclined, dependently-typed-curious' programmer, offering a (more shallow) stepped path from List to Any might prove to be positive propaganda on our behalf!

[Saransh-cpp]

I think I forgot to post a reply here yesterday (I remember I wrote one 😬)

deleteAt appears to be the ─ operation?

I missed that! Thanks!

this may be yet another knock-on consequence of List and Vec not being mutually consistent

I found a lot of such inconsistencies yesterday. For instance, starting with the insert, delete, and update operations, Vec and List have some of them as functions and some of them as mixifx operators making it very inconsistent -

• Vec has both a function and a mixifix operator for updating an element using a function (updateAt and _[_]%=_), List has only the mixfix operator
• For removing an element, Vec only has remove, on the other hand, List has a mixfix operator _─_, making this also inconsistent with the "update" function and operator
• For insertion, Vec has insert and List has nothing.

  insert : Vec A n → Fin (suc n) → A → Vec A (suc n)
  remove : Vec A (suc n) → Fin (suc n) → Vec A n  -- similar to _─_ in List
  updateAt : Fin n → (A → A) → Vec A n → Vec A n
  _[_]%=_ : Vec A n → Fin n → (A → A) → Vec A n  -- this is updateAt, but as a mixfix operator
  _[_]≔_ : Vec A n → Fin n → A → Vec A n -- overwrites the i-th element of xs with y

_[_]%=_ : (xs : List A) → Fin (length xs) → (A → A) → List A  -- similar to Vec, but does not have the updateAt function
_[_]∷=_ : (xs : List A) → Fin (length xs) → A → List A  -- similar to Vec
_─_ : (xs : List A) → Fin (length xs) → List A  -- similar to remove in Vec, but List does not have a remove function

I'll start by making these 3 functions and their corresponding mixfix operators consistent.

---

Reading your thoughts about association lists, I think it is more complicated to add them to Agda than I had initially thought 🙂

I read about association lists and if I understood your comments, association lists do not exist in Agda? So this would require formalising the idea and API of association lists in Agda before actually writing those functions.

Let me update this issue to discuss only association lists. I will create another issue/PR for the Vec and List inconsistency.

[jamesmckinna]

To tidy up my ramblings: I don't think we implement (key,value) association lists, with arbitrary key -> value -> bool-based lookup, anywhere in the library. But we do do so, for decidable-equality key-based lookup, for finite Maps via AVL trees.

As to the latter, I have in #1911 suggested that we take seriously the design of a suitable (for the dependently typed context) API for Map-like things (so association-lists would be another possible instance/implementation), but that suggestion hasn't been taken up (yet, AFAIK).

As to the former (and perhaps, in the context of the issue, against implementing association lists per se, but read on...) it occurred to me/I conjectured that, with sufficient ingenuity, the arbitrary key-value relation-based (Boolean-valued, or otherwise) lookup etc,. on association lists could be implemented using the 'intrinsic' definition/properties of Any.lookup. Such a conjecture, if considered 'interesting enough', ought to be testable/tested... ;-)

But that might seem a 'what's the point?' question (is it interesting enough?)

Except that, for didactic purposes, I think that a demonstration of the power of dependently-typed programming (via Any, suitably specialised) might be a very useful 'propaganda' contribution ... "on the unreasonable effectiveness of Any" ;-) ... so not necessarily as a library contribution, perhaps, unless under README? One for further discussion, I think!

ADDED: Matthieu Sozeau's early paper (2008?) on finger trees in Coq might make a useful comparative case study...?

[MatthewDaggitt]

See https://github.com/agda/agda-stdlib/pull/1552 for a discussion of an aborted attempt of designing a similar interface for priority queues.

[jamesmckinna]

Regarding @MatthewDaggitt 's comment: my own instincts are also towards a wide user-facing API, with a narrower implementor-facing API, not least because we are/have become more sophisticated about 'smart constructor' approaches to bootstrapping from narrow to wide... although I'm not immediately clear about how best to implement haskell type class-like default implementations, on a per-field basis (rather than monolithically)

But in some sense, the API design question (and any subsequent PR) can (ought?), conceptually at least, be uncoupled from implementation... even if any particular experiment will probably ping-ping iteratively between the two! The challenge of collaborative software development might be to remain, as far as possible, as flexible/ego-less as regards API revision, as possible. Mind you, that's rich coming from me!

[JacquesCarette]

So I looked at Any in relation to this, and I get the feeling that it is 'backwards' in the sense that if you have an Any in your hands, you already have the answer you seek with doing a lookup in an association list. So what would be the point?

The main point of this issue is to ask: should agda-stdlib have association lists? That exact structure, rather than the wider question of designing a generic API for key-value stores.

[JacquesCarette]

To go to things said way back at the start of this thread: I'm explicitly choosing to discuss this on issues here, so that there is written record of the discussion (and ultimately the results of that discussion) that can easily be searched in the future.

I'm not sure if enough of the designers of stdlib spend enough time on the Zulip to have a 'better' conversation there. Ultimately, it is the quality of the conversation that matters most.

[jamesmckinna]

@JacquesCarette thanks for the nudge use of the issue tracker for these open-forum discussions. Against myself, I perhaps even agree that the Zulip might not be the right place, although it (and other Zulip instances) is where I spend a lot of time online these days, outside my own contributions to development here.

[jamesmckinna]

To the discussion topic then: my understanding is that we don't have association lists per se in the library.

If they are to be added, I might think under Data.List.Association.Base and Data.List.Association.Properties, with some possible axes in the design space to consider:

• vanilla key × value pairs stored in the lists, or something more interesting? (eg should values be able to depend on keys?)
• types in the 'basic' API: haskell-like ('haskellic'? 'haskeletal'?) as in #2042 , or more dependently-typed/richly articulated? (in an ideal world, we might seek PRs offering each extreme, and cherry-pick the best-of-breed?)
• what properties do we want?

This, in turn, might generate, here or as a separate issue/PR, an API ... (oh, I can be very top-down as a designer, can't I?)... and once we agree, a PR implementing it. But then @MatthewDaggitt 's mention of #1552 and #1542 and earlier discussions about narrow/wide API design come to the fore...

... but would you (two; @JacquesCarette and @Saransh-cpp ) like to start the ball rolling? (no pressure, express or implied)

[jamesmckinna]

Another one to punt until after v2.0, I think ;-)

[jamesmckinna]

I would love it if we had (collectively) had time to pursue this discussion further, but suggest removing from the v2.1 milestone, at least, if not closing entirely...?

[JacquesCarette]

I agree, this seems quite stale. I will have another student working on stdlib this summer. Still, this may not be the highest priority then either.