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.

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

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

   1. K1 :: K2
   2. 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}.