Domain keys in map

[gldubc]

This allows maps to encode domain keys, from paper https://www.irif.fr/~gc/papers/icfp23.pdf

For example, we can now express the type %{a: integer(), b: float(), atom() => tuple()} of maps that have keys :a and :b and any other atom key mapping to a tuple.

Those are created by adding {{:domain_key, :atom}, type} pairs to constructors open_map or closed_map.

This introduces new operators:

• map_get, which computes the type obtained with expression map[key] where key is some expression of some type
• map_refresh, which computes type the map obtained when doing Map.put(map, key, type) (not called map_put because the name is already used for adding a single key to a map. The difference here is that, key being a type, we are not sure which key is being added).

Both operators handle singleton atoms exactly. See the following tests:

 test "more complex map get over atoms" do
      map = closed_map([{:a, atom([:a])}, {:b, atom([:b])}, {{:domain_key, :atom}, pid()}])
      assert map_get(map, atom([:a, :b])) == {:ok_present, atom([:a, :b])}
      assert map_get(map, atom([:a, :c])) == {:ok, union(atom([:a]), pid() |> nil_or_type())}
      assert map_get(map, atom() |> difference(atom([:a, :b]))) == {:ok, pid() |> nil_or_type()}

      assert map_get(map, atom() |> difference(atom([:a]))) ==
               {:ok, union(atom([:b]), pid() |> nil_or_type())}
    end

  # Tricky cases with atoms:
  # We add one atom fields that maps to an integer, which is not :a. So we do not touch
  # :a, add integer to :b, and add a domain field.
      assert map_refresh(
               closed_map(a: pid(), b: pid()),
               atom() |> difference(atom([:a])),
               integer()
             ) ==
               {:ok,
                closed_map([
                  {:a, pid()},
                  {:b, union(pid(), integer())},
                  {{:domain_key, :atom}, integer()}
                ])}

Notes:

• I have not tested enough the optimizations to know if they can be adapted to domains.
• One operator missing is map_delete.
• Function map_check_domain_keys(tag, neg_tag) is very long to treat all the different cases optimally. It could be shortened to a single loop on all the possible domains, with default values.

[josevalim]

I will lock this issue for now because of spam, will reopen once I have feedback. :(

[josevalim]

I wonder if we should simply have the tag be either: :open, :closed, or domains. If you have a map as the tag, then it has domains key. If an open map, then we expand everything, as done in map_with_default.

[gldubc]

Yes it's possible to do so, the benefit of keeping them is just so we can represent {:open, domains} without putting a top type in all the undefined domains. But it does not give us much more.