association lists, finmap

Stream: general

[Sean Leather]

As some people know, I've been working on association lists and finite maps for mathlib (https://github.com/spl/lean-finmap). Mario has decided he wants to get it into mathlib soon, so he has started rewriting it in his own fashion (https://github.com/leanprover-community/mathlib/tree/finmap). I wanted to open up the discussion to get feedback from anyone else who might be interested.

[Sean Leather]

One question is whether there is the need for a structure to wrap a list without duplicate keys. Mario thinks it might be useful:

structure alist (α : Type u) (β : α → Type v) : Type (max u v) :=
(val : list (sigma β))
(nd : val.knodup)

https://github.com/leanprover-community/mathlib/blob/e5ddd1d4dca984f6d7a77a87a1608b414296208f/data/list/alist.lean

I went down this path and found that, given that (a) there are so many useful definitions and theorems regarding lists and (b) the structure is such a thin wrapper, every definition or proof for the structure is simple, it created a large number of really simple statements. Considering that alist is really a list with a property and I believe it is useful to use other list definitions that don't involve this property, I think the alist structure either (a) makes it more difficult to work with the wrapped list or (b) creates the problem of scaling the number of statements about alist to match those already about list.

[Sean Leather]

In another way of putting it, you could look at an alist as something unique on its own or you could look at a list with a property that it has no duplicate keys. In the process of developing my library, I found the latter view much more useful.

[Simon Hudon]

Why is latter more useful?

[Sean Leather]

On a related note, that's also how I ended up with the finmap structure:

structure finmap (α : Type u) (β : α → Type v) : Type (max u v) :=
(val : multiset (sigma β))
(nodupkeys : val.nodupkeys)

https://github.com/spl/lean-finmap/blob/035f1faa218e47b9f411c4a243900955f4714a56/src/data/finmap.lean#L8-L10

You could say that this is a similar situation: a finmap is just a multiset with no duplicate keys. However, I found that it's more useful to look at it as a finmap because I didn't find a lot of the other multiset definitions to be very useful for a finmap.

[Sean Leather]

Why is latter more useful?

The most important reason for me is that I care about the structure of the internal list: nil, cons, append, etc.

[Sean Leather]

Also, regarding finmap, I don't care about the structure of the internal multiset.

[Sean Leather]

... which makes sense, since a multiset is a quotient.

[Sean Leather]

@Simon Hudon Thanks for that question, BTW. It gets to a key reason I don't think alist is useful, a reason that hadn't yet come to mind.

[Sean Leather]

That is, I found that it was useful to wrap a quotient like multiset in a structure but not that useful to wrap a list in a structure because the structure of the list is important when working with the structure. I ended up creating definitions to wrap nil, cons, append, etc., and all of that already existed for the list, so I came to ask why it was necessary. I couldn't come up with a good answer.

[Simon Hudon]

You could say that this is a similar situation: a finmap is just a multiset with no duplicate keys. However, I found that it's more useful to look at it as a finmap because I didn't find a lot of the other multiset definitions to be very useful for a finmap.

I don't get this nuance

[Sean Leather]

I don't get this nuance

I think it's similar to how you don't see a lot of the multiset definitions used for finset. There's a particular subset (mostly starting with nd) that are used in finset, but many of them are not.

[Sean Leather]

multiset seems to be useful as a substrate for finset and finmap, but it also has a larger API that is oriented towards counting duplicates.

[Sean Leather]

Also, the subset of the multiset API used for finset is not useful for finmap.

[Mario Carneiro]

I think the comparison is apt, and applicable to alist. A finset is just a multiset with a property, but the API is different (some basic operations are not applicable, like cons, and others are slightly weird and become more useful on the subtype, like ndinsert).

[Mario Carneiro]

In the case of alist, there are some operations that don't work anymore, like cons, and others are slightly weird and have been prefixed with k for lists. cons is just not a valid alist operation, insert is.

[Sean Leather]

I think the comparison is apt, and applicable to alist.

So does this mean you agree with me, since my comparison is apt, which is to say that alist is not a useful structure?

[Sean Leather]

In the case of alist, there are some operations that don't work anymore, like cons, and others are slightly weird and have been prefixed with k for lists. cons is just not a valid alist operation, insert is.

This hints of disagreement. My point is that lists are constructed with nil and cons, and it is useful to have that construction, and therefore more useful to have a bare list with no duplicate keys than to have a structure hide that construction.

[Mario Carneiro]

In short: I think finset is useful, and I think alist is useful

[Mario Carneiro]

I don't see why alist should provide a nil/cons construction. It's not natural. If you want to do such a construction then you should unpack the alist first

[Sean Leather]

That's kind of my point. :wink:

[Mario Carneiro]

Instead it has empty/insert

[Mario Carneiro]

My point is, why are you doing list things on alists?

[Sean Leather]

My point is that I want to construct lists with no duplicate keys as well as use any other existing definitions and theorems on lists.

[Mario Carneiro]

then do so, on list. You don't need alist for that

[Sean Leather]

Quite right, which is why I don't think alist is necessary.

[Mario Carneiro]

alist provides a compositional structure for safety-preserving functions on lists

[Mario Carneiro]

as well as use any other existing definitions and theorems on lists.

Most list operations don't preserve the invariant. What do you do with these?

[Sean Leather]

Well, if you want it, add it. I'm only trying to save you work.

[Mario Carneiro]

This is an honest question. What is missing from the API of alist that you would want, that requires resorting to list?

[Mario Carneiro]

Except for union, there's nothing I've missed that comes to mind

[Sean Leather]

I'm not sure about alist, but I defined the minimum necessary to use lists with no duplicate keys. For example, has_mem and append don't need to be redefined. You only need some extra properties to use append, for example.

[Mario Carneiro]

To answer your question from earlier, alist should also be available as a tool for programmers. "I need a map, I only have equality" -> use alist or finmap

[Mario Carneiro]

Note that the has_mem on alist is different from the one on lists

[Mario Carneiro]

and append doesn't apply

[Sean Leather]

Which I don't think it should be.

[Sean Leather]

As you'll see in my library.

[Mario Carneiro]

I think in common programming parlance, x \in m where m is a dictionary / map / associative array, means x is a key contained in the map m, not x is a key-value pair in the map

[Mario Carneiro]

The idiom for the other interpretation is <x, y> \in m.val, where val is the operation sometimes called entries in other libraries

[Mario Carneiro]

(indeed, maybe it should be renamed to that)

[Mario Carneiro]

Note also that if it meant membership in the underlying list, then it wouldn't be decidable unless you assume decidability of the values, which is not needed for anything else

[Sean Leather]

Fair enough. With a : alist, you can use a.val/a.entries.

[Mario Carneiro]

right, I think this helps to view them as different things (a finite map vs a list of pairs)

[Mario Carneiro]

You pointed out that it is possible to define operations like append if you assume side conditions (i.e. the key sets are disjoint). Does this come up often?

[Sean Leather]

I don't know about “often,” but it has come up.

[Sean Leather]

I'm now using finmap instead of association lists directly, and you have the same thing with union there.

[Sean Leather]

I'm assuming you'll use has_union for alist instead of has_append?

[Mario Carneiro]

yes

[Mario Carneiro]

since it's union, not append :P

[Mario Carneiro]

it's not even possible to give an append instance that uses list.append

[Sean Leather]

Well, it's debatable that it's not a form of append.

[Mario Carneiro]

I prefer set terminology when duplicates are being dropped

[Sean Leather]

It's still appending. :slight_smile:

[Sean Leather]

When it comes to the finmap, you can forget that there is any appending. But with alist, you can't.

[Mario Carneiro]

Not sure what you mean. The underlying operation is not an append

[Mario Carneiro]

It is true that union would be order-respecting on alist

[Mario Carneiro]

but then again, so is union on list

[Sean Leather]

def append : list α → list α → list α
| []       l := l
| (h :: s) t := h :: (append s t)

def kunion : list (sigma β) → list (sigma β) → list (sigma β)
| []         l := l
| (hd :: tl) l := hd :: kunion tl (kerase hd.1 l)

[Sean Leather]

Are you doing it differently?

[Mario Carneiro]

I think the erase makes that a rather different kind of operation. But also I think we need two functions here - that is unionl

[Mario Carneiro]

unionr would be

def kunionr : list (sigma β) → list (sigma β) → list (sigma β)
| []         l := l
| (hd :: tl) l := kinsert hd.1 hd.2 (kunionr tl l)

[Mario Carneiro]

I'm not even sure if it should get a has_union notation

[Sean Leather]

I'm not sure if you need it. I don't foresee people asking for it.

[Mario Carneiro]

You need left and right preference. For finmap you can ignore it since the order of parameters gives the preference, but on alist you have order and preference separately

[Sean Leather]

Why do you need it? Just because it's possible doesn't make it a need.

[Mario Carneiro]

I'm okay with just assuming right preference (which is what list.union does), but you want left preference?

[Sean Leather]

I stuck with the Haskell Data.Map approach because it seemed to the most intuitive to me.

[Mario Carneiro]

Keep in mind that haskell has laziness to contend with, making your definition more natural for them

[Sean Leather]

Yep.

[Sean Leather]

∪ is infixl, so could that also indicate left-biased is preferred?

[Mario Carneiro]

It seems like the difference between foldl and foldr

[Mario Carneiro]

and we have both of those

[Mario Carneiro]

I'd rather not commit to one camp here

[Mario Carneiro]

particularly since there are also performance characteristics to worry about, and the lean 4 compiler may change this as well

[Sean Leather]

You have to commit to one for ∪ at the very least.

[Sean Leather]

I guess if you're going with the list.union precedent, you would go with the right-biased option.

[Mario Carneiro]

I think alist shouldn't have a notation, finmap can use left preference by default since the API properties take precedence there

[Mario Carneiro]

I should look at other languages like java or python and see what preference is preferred

[Sean Leather]

I would consider Haskell, ML, OCaml, Coq, Agda, Idris, etc. before looking at Java or Python.

[Mario Carneiro]

hm, python has a mutation operation which makes the precedence obvious

[Mario Carneiro]

Same with java. OCaml takes a merge function that resolves differences

[Mario Carneiro]

Haskell has both union (left bias) and unionWith that takes a merge function

[Mario Carneiro]

I couldn't find anything for Coq. Idris uses merge left bias and mergeWith

[Mario Carneiro]

ML is roll your own dict

[Sean Leather]

I'm coming to realize that what would be better for me than a finmap union that updates by insert or erase is something like an internal disjoint union. At least that's what I've gathered it would be called. [1, 2] For finmap, perhaps the simplest definition would be:

def djunion (f g : finmap α β) : finmap α β := if disjoint f.keys g.keys then f ∪ g else ∅

But a more efficient version would probably use list.append instead of list.kunion as ∪ does.

I'm only dealing with unions of disjoint finmaps, and it would simplify some things if I didn't have to track all of the disjoint f.keys g.keys.

[Sean Leather]

Likewise, a disjoint insert would be good. Conceptually:

def djinsert (a : α) (b : β a) (f : finmap α β) : finmap α β := if a ∉ f.keys then insert a b f else ∅

But cons would be better than kinsert.

[Sean Leather]

@Mario Carneiro What is your plan with https://github.com/leanprover-community/mathlib/tree/finmap ? I'd like to see something get into mathlib. However, given the somewhat large difference between your rewrite and my library, I'm a bit reluctant at this point to invest the time to port more definitions and theorems over to that branch without knowing what's going to happen to it. Do you plan to continue working on that branch?

[Mario Carneiro]

would you like me to merge it?

[Sean Leather]

would you like me to merge it?

“It” being the leanprover-community/mathlib branch? Sure, if you're happy with it in its current state. I would feel more comfortable extending it at that point.

[Mario Carneiro]

I noticed you renamed some things. Not a fan of knodup?

[Sean Leather]

I noticed you renamed some things. Not a fan of knodup?

:slight_smile: No. I think nodupkeys is better.

[Mario Carneiro]

when I look at it I think "nine letters is long for a name segment"

[Mario Carneiro]

You could have nodup_keys but then it confuses with nodup of keys

[Mario Carneiro]

what about nodup_fst?

[Sean Leather]

You could have nodup_keys but then it confuses with nodup of keys

Exactly.

[Sean Leather]

what about nodup_fst?

How is that better than nodupkeys since nodup and keys already exist?

[Sean Leather]

... exist in the association list/finmap API that is.

[Mario Carneiro]

I mean for the list version, before the "map" interpretation

[Sean Leather]

I'd prefer nodupkeys for both for consistency's sake. I think the name is clear in that it links nodup and keys and as short as it's needed to be.

[Sean Leather]

Anyway, I have to go now. If you want to discuss any other issues, I'll pick it up tomorrow.