Map types

Introduction

Map types can have optional associations K => V and mandatory associations K := V.

If a map type doesn't mention a key of a certain type, such keys are forbidden in maps of that type. For example, #{} is the empty map, so if a map value has any key at all, it is not a value of type #{}.

Map types have the same syntax as map expressions, but with a different meaning of => and :=, which may be confusing. We'll try to always use the words map type when we refer to a map type.

Subtyping

Subtyping for map types needs some documentation. Here is a draft.

A for subtyping in general, T1 is a subtype of T2 if all values/expressions/patterns of type T1 are also values/expressions/patterns of type T2. We use T1 :: T2 to denote subtyping. (It is actually compatible subtyping.)

Map type examples

• Type #{}: The empty map type has only one value: The empty map #{}. No keys are allowed.
• Type #{a := b}: A map with a mandatory key of type a which maps to a value of type b. There is only one such map: #{a => b}.
• Type #{a => b}: A map with an optional key a, so it has two values: #{a => b} and #{}.

We can see that #{} :: #{a => b} and #{a := b} :: #{a => b}.

Subtyping rule

M1 :: M2 if and only if for all associations K1 <Assoc1> V1 in M1, there exists an association K2 <Assoc2> V2 in M2 such that

1. K1 :: K2,
2. V1 :: V2,
3. <Assoc1> must be mandatory if <Assoc2> is mandatory,
4. the association K2 <Assoc2> V2 must be the first association in M2 matching a key K2 such that K1 :: K2,

The third requirement means that {Assoc1, Assoc2} must be one of the following three combinations: {=>, =>}, {=>, :=} or {:=, :=}.

The forth requirement accounts for the "The key types in AssociationList are allowed to overlap, and if they do, the leftmost association takes precedence" in Erlang Types and Function Specifications.

Mandatory associations with non-singletons key types

A mandatory key is typically a singleton such as a specific atom or integer, but what if a mandatory association is used for a non-singleton type as the key? We interpret it as only one key of the type is required.

Example: The type #{a | b :: c} is a map type where a key of type a | b is mandatory, i.e. a or b. Thus, the values of this type are #{a :: c}, #{b :: c} and #{a :: c, b :: c}.