DAML-LF: GenMap Spec

[remyhaemmerle-da]

In this PR we specify the operational semantics of GenMap builtin.

This advance the state of #2256

Pull Request Checklist

• Read and understand the contribution guidelines
• Include appropriate tests
• Set a descriptive title and thorough description
• Add a reference to the issue this PR will solve, if appropriate
• Include changelog additions in one or more commit message bodies between the CHANGELOG_BEGIN and CHANGELOG_END tags
• Normal production system change, include purpose of change in description

NOTE: CI is not automatically run on non-members pull-requests for security
reasons. The reviewer will have to comment with /AzurePipelines run to
trigger the build.

[ghost]

One question that the spec should answer: does it raise a runtime error when inserting a value that is incomparable in an empty map? (I think it should raise an error, for the sake of consistency.)

[remyhaemmerle-da]

It does not.
It raise an exception exactly once LESS or EQUAL does.

We agreed with @hurryabit and @hurryabit that is the only semantics that is reasonable. Otherwise you will have to always traverse all the keys to ensure there is no function nested inside.

Imagine you have the type

data D = 
    FUN (Int -> Int) 
  | INT Int

You can insert (Fun (\x -> x)) in any GenMap that does not content Fun variant.
You can also try to lookup the entry of key (Fun (\x -> x)) without raising an exception in any GenMap that does not content Fun variant.

However as soon you have an entry with a key (Fun ...) in your map you cannot do anymore any operation that invole a other key of the form (Fun ...) without raising an exception.

This choices is simpler and more efficient. Furthermore the compiler will never produce such case.

[ghost]

Ok, if @hurryabit and @hurryabit can confirm ;-)

The reason I don't like this is that you are creating the potential for latent runtime errors when you perform inserts -- i.e. creating a runtime error that will only be found on a subsequent lookup, instead of when the real error occurs. This is particularly bad for e.g. people using genmaps during testing, or choice validation.

When adding a new key to the map, It should be easy to compare a key to itself using EQUAL, to make sure it doesn't introduce latent runtime errors.

[ghost]

In the proposed semantics, you are only saving 1 comparison, but you are introducing latent runtime errors, so I don't think it's worth it.

[cocreature]

It depends on what kind of values you have. If you have ADT-like trees, being able to short circuit on comparisons can make a pretty large difference. Given that we prevent this runtime error in DAML, I’m not sure that missing out on better performance here in favor of “nicer semantics” for DAML-LF is worth it. That said, I don’t feel particularly strongly about this.

[remyhaemmerle-da]

In fact, @associahedron I like your proposal.
The advantage I see, is that we can switch the implementation to hashmap, if we realize the implementation is too slow (we will sorted the map only for serialization).

In other words, in each case (insertion, deletion and lookup) we check the value is equal to itself. Hence we have a nice definition of "comparable" value.

[ghost]

@cocreature If you use nested trees as keys, maps are going to be slow regardless. I'm also not confident that this case will never ever occur at runtime in DAML.

@remyhaemmerle-da 👍

[cocreature]

Alright, then let’s error out for now.

[ghost]

Spec should say what happens in the case of empty map lookup of incomparable keys. (I favor more runtime errors.)

[ghost]

At lookup it is not super critical to check the key for self-equality, but I think that at insertion time it is more important.

[remyhaemmerle-da]

no error ;)

[ghost]

if you want to leave the possibility for hashtable-based implementation open, you should error on bad lookup keys

[remyhaemmerle-da]

As agreed in previous thread, we raise an error

[ghost]

Thanks! This spec looks good, but we need to be explicit about what happens with empty maps.

[ghost]

You can simply reinstate this paragraph if you want to leave the possibility for hashtable-based implementation open (but use EQUAL instead of ~ᵥ).

[remyhaemmerle-da]

done

[ghost]

Approving since the missing insert rule was added, and we've discussed about the merits of error-ing on incomparable keys (I leave the final decision to you).

[remyhaemmerle-da]

Thanks @associahedron for this constructive discussion. I believe it is better now.