assoclist model

Stream: batteries

[James Gallicchio]

hey all, I'm working on getting assoclist into the leancolls abstraction circus, but I'm realizing that it is actually a rather annoying dictionary because of the whole deduplication thing.

in particular, one of the things we do in leancolls is connect membership (hereAssocList.find?) with fold (here AssocList.foldl). But for AssocList they are always going to disagree if we don't require deduplication.

so, how do you use assoclist, and what does "correctness" mean to you for assoclist?

[James Gallicchio]

I guess another question is whether you find it surprising (even if not too hard to see) that AssocList.fold "disagrees" with AssocList.find?, in the sense that it will fold over key-value pairs that are not in the dictionary according to find?

[Mario Carneiro]

Have you seen docs#AList ?

[Mario Carneiro]

AssocList is not suitable as a dictionary on its own, you want to pair it with a NodupKeys assumption to be usable

[Mario Carneiro]

AssocList is just a funny looking List

[James Gallicchio]

is anyone proving code with AssocList?

(or using AList for programming purposes? I thought the issue with AList was the performance hit from the extra indirection)

[Kim Morrison]

I have a branch of Std (std4#556) in which I added a keysOrdered predicate to AssocList, that

• asserted that according to some order the keys were strictly ordered
• gave some variants of operations which assumed / ensured this condition
• and some theorems about these operations.

However my target application dropped off the priority list, so the PR is incomplete. If it's useful I can revive it or hand it off.

[James Gallicchio]

ooooh, okay, I may snatch this into leancolls if that is alright with you...

[Kim Morrison]

Yes please!

[James Gallicchio]

(I could probably also maintain an assoclist variant that just scans the full list and maintains a nodupkeys invariant rather than an order invariant, so that the keys don't need to be ordered. but if there's no use case for unordered keys, I see no reason to maintain both...)

[Kim Morrison]

I was initially working on this because the current implementation of omegajust uses List Int to represent coefficients of linear forms (i.e. a dense representation), and wanted to replace it (because someday someone will run omega with thousands of variables, and the current implementation will fall over). We decided to do a more thorough replacement of omega, so if something usable appears in the meantime everyone will be happy. :-)

[Kim Morrison]

I'd be inclined to go straight to ordered.

[François G. Dorais]

Ordered keys is more useful when based on Array rather than List. This is because Array.get is O(1) so binary search makes AssocArray.get O(log n). Since List.get is O(n), AssocList.get is O(n) regardless of order.

[James Gallicchio]

actually, I just realized the hashmap buckets are assoclist with nodup keys, right? maybe it's worth maintaining then. hm.

[Mario Carneiro]

Note that the nodup key proof is stored separately from the assoc list itself, and after std4#748 (or some variant) lands this seems unlikely to change