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, 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.

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

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

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

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]
   • 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}.