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 type, 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 and patterns, but with a different meanings of => and :=, which may be confusing. We'll try to always use the words map type when we refer to a map type.

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 #{}.

Map Expressions

The most specific type of the expression {a => b} is the type #{a := b}, since it contains only this and nothing else.

A map update expressions such as M#{a => b} or M#{a := b} has the same type as M, with the addition a := b. If the key a is already in the type of M, it is replaced by a := b in the result type.

Map Patterns

A pattern such as #{a := b} matches any map associating the key a to the value b, regardless of whether the value tested against this pattern is a map which also contains other keys and values. Thus, the pattern matches all values of type #{a := b, any() => any()}. (In some projects, such types are written using underscores for the catch-all association #{a := b, _ => _}.)

Subtyping

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

As 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.)

For the examples above, we can see that #{} :: #{a => b} and #{a := b} :: #{a => b}.

Subtyping rule, short version

For a map type M1 to be a subtype of another map M2, there are two conditions to be fulfilled:

1. All the allowed key in M2 must also be allowed in M1 and the associated values have to be subtypes of each other and
2. All mandatory keys in M1 must also be mandatory in M2.

Subtyping rule, long version

Given two map types M1, M2.

M1 :: M2 if and only if the following two conditions are fulfilled:

1. For all associations K1 <Assoc1> V1 in M1, there exists an association K2 <Assoc2> V2 in M2 such that

   • K1 :: K2,
   • V1 :: V2,
   • <Assoc1> is mandatory if <Assoc2> is mandatory, [Deleted, since we have condition 2 below for mandatory associations. Is it correct to delete this bullet? /Viktor]
   • the association K2 <Assoc2> V2 is the first association in M2 with a matching a key K2 such that K1 :: K2.

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

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

2. For all mandatory associations K2 := V2 in M2, there is a mandatory association K1 := V1 in M1 such that

   • K1 :: K2
   • V1 :: V2

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 that at least 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}.