Add GenMap to DAML-LF 1.dev spec

[ghost]

This PR advances the implementation of #2256.

It introduces a new 'GenMap' primitive type in DAML-LF that generalizes the 'Map' primitive type. Here's a comprehensive summary of the differences between the two types:

• 'GenMap' takes two type arguments: the type is 'GenMap' k v instead of 'Map' v. The first type argument to 'GenMap' is the key type for the map, where the original 'Map' type only supports 'Text' keys.

• All the operations on 'GenMap' k v are the same as for 'Map' v except:

  • They are labelled GENMAP_EMPTY, GENMAP_INSERT, GENMAP_LOOKUP, GENMAP_DELETE, GENMAP_KEYS, GENMAP_VALUES, and GENMAP_SIZE, instead of MAP_*.

  • They take two type arguments (the key type and the value type) as opposed to MAP_* operations that only take one type argument (the value type).

  • Because we're phasing out LF tuples, we have GENMAP_KEYS and GENMAP_VALUES instead of GENMAP_LIST. These return a list of keys or values in the order that the items were inserted (rather than in alphabetical order by key). This is because keys can contain Contract IDs, which do not (and cannot) have a predetermined order, and we want the output of GENMAP_KEYS/GENMAP_VALUES to be deterministic regardless of the assignment of Contract IDs.

  • GENMAP_INSERT, GENMAP_LOOKUP and GENMAP_DELETE cause a runtime error whenever they are passed an invalid key, unlike MAP_* operations which can never cause a runtime error. See below for the definition of "invalid key".

  • Key comparison for GENMAP_INSERT, GENMAP_LOOKUP and GENMAP_DELETE is defined according to a key comparison relation ~ᵥ that generalizes text key equivalence. See below for the definition of this relation.

• We define a generic partial equivalence relation ~ᵥ to be used for key comparison that generalizes the equality relation for all built-in types, and extends it to lists, optionals, enums, variants, record and tuples. It doesn't rely on type information at all, so we maintain type erasure. This relation is not exposed as a built-in operator.

• We define a key to be valid iff it is equivalent to itself according to the key comparison relation ~ᵥ. This excludes all functions, type abstractions, update/scenario monads, and any composite value that contains them, from being considered valid keys. It also guarantees that ~ᵥ is an equivalence relation over all valid keys.

[cocreature]

Looks great, nice work!

[hurryabit]

I like the constructive nature of this very much. Thanks for pushing into that direction!

[remyhaemmerle-da]

First draft looks good to me.

[remyhaemmerle-da]

You are forgetting the "nice" case where keys are maps.
Of course we can a first implementation without map keys.

[ghost]

That's not nice! We probably will need to add them, but I'm worried the "insertion order" issue will mess people up.

But also I don't see map values under the values section (including 'Map'). Probably should add them?

[remyhaemmerle-da]

We can postpone this problem for later.

[remyhaemmerle-da]

TextMap (simply called 'Map' in the spec) are not concern with the insertion order.
They are sorted by key when converted to list or serialized in the ledger.

[ghost]

Right. I propose that two 'Map' (i.e. TextMap) are considered equal if they have the same key-value pairs, and two 'GenMap' are considered equal if they have the same key-value pairs in the same insertion order, so they result in the same output when using GENMAP_KEYS and GENMAP_VALUES.

[remyhaemmerle-da]

OK. Let's start without it. We can still add it letter.

[hurryabit]

I'm not averse to removing user-defined equality from DAML. Particularly if we find a way to keep the Eq type class as a marker but have no (or at least no user-implementable) methods in it. I'm not sure if that feasible though since Eq is probably wired quite deep into GHC.
@associahedron do you have some time at hand to investigate this a bit?
@bame-da what do you think about this?

[ghost]

@hurryabit I think we can outlaw custom Eq instances in the preprocessor, and tell users to use deriving Eq instead.

[ghost]

We could make it a warning for a while, and turn it into an outright error later.

[hurryabit]

That sounds reasonable to me. We should then also replace the derived Eq instances with calls to our DAML-LF primitive during our conversion to DAML-LF.

[ghost]

Updated the spec with reviewer comments.

[remyhaemmerle-da]

LGTM