Map Lattice

[derekelkins]

I may make a PR for this, but, in addition to the Set lattice, another natural instance is for (a wrapper around) BTreeMap/HashMap. Mathematically, functions into a lattice form a lattice pointwise. We can view a map as a partial function from keys to (lattice) values and then make it total by mapping into Option which we view as freely adding a bottom element (and this is how the trait implementation for Option behaves).

The upshot is the obvious implementation where we union/intersect the keys and use join/meet for any keys in both maps is a lattice corresponding to the mathematical description above. Indeed, the Set lattice is exactly this Map lattice with the values being the () lattice. A nice consequence of this is tries with values in lattices become a lattice too "automatically".

That is,

struct Trie<K, L>(Product<(L, Map<K, Box<Trie<K, L>>>)>);

has a simple Lattice implementation that just delegates to its interior type.

(A bit of an aside, egglog takes the view that maps/partial functions into a lattice rather than relations are the primitive notion with relations being viewed as maps into (). I find this perspective, which could perhaps be supported by alternative notation, e.g. lattice shortest_path(i64, i64) := Dual<u32>;, to be more self-explanatory.)

[s-arash]

I think we can add that. But I'm curious, wouldn't that be isomorphic to pulling out the Map key into a new column of the ascent lattice?

What I mean is: If you have

  lattice foo(A, Map<B, C>);

wouldn't that be isomorphic to

  lattice foo(A, B, C);

?

It looks like the former is the curried form of the latter.

Maybe there is something I'm missing here though, as I haven't thought about it much.

[derekelkins]

There are some differences, but you're right. Taking the view of (lattice) relations as lattice-valued functions, what you describe is exactly the analogue of currying. More specifically, it's like Map<(K1, K2), V> ~ Map<K1, Map<K2, V>>. By the same logic, lattice foo(A, Set<B>) is similar to lattice foo(A, B, ()) or relation foo(A, B).

Of course, what currying gives us is higher-order lattice relations. We can store those Maps somewhere and use them later. An extreme rendition of this is Datafun which you're aware of. Maps also provide one route to represent monotonic aggregations which can be done even more efficiently using the ideas of lattice morphisms and monotone maps as described in the Bloom^L paper. Table 3 in that gives a nice summary of various lattice morphisms and monotone operations for various lattices.

Higher-order lattice relations have similar benefits to higher-order functions in allowing common logic to be abstracted. As a mildly silly example:

lattice failed_any(Map<Course, Dual<Grade>>, bool);
failed_any(m, m.map_monotone(|g| g.0 <= 69).join());

failed_any is a non-trivial monotonic aggregation and can be used for any collection of course grades. Without Map you would need to duplicate the failed_any logic for each use, i.e.:

some_lattice_rel(x, y, m);                                failed_any_some_lattice_rel(x, y, g.0 <= 69) <--
failed_any(m, b);                  would become               some_lattice_rel(x, y, _, g);

[s-arash]

Ah, you are absolutely right. In fact, that is exactly what we did in the BYODS paper (see section 5.6). There, we defined a MapLattice data type to use for recursive aggregation.

If I'm not mistaken, the Map type you are proposing would be the same MapLattice type that we defined in the paper. If that's the case, we can add the type to Ascent (it wouldn't be difficult for users to define the type themselves, but as it appears to be worthwhile addition to Ascent).