map_spec_extension_proposal.md

Current Syntax

Existing map specification syntax, as was introduced in 17.0, allows the following different syntaxes:

• map() or #{}: the type of any map (of any size).

• #{a => integer(), b => list()}

  A map that may only contain keys a and b. If it contains a key a, then it must be mapped to an integer value. Analogously for b.

• #{binary() => integer()}

  A map with 0 or more mappings, where all the keys are of type binary() and all values are of type integer().

Problems With It

Consider the following example from the Maps EEP:

func(inc, #{status := update, c := C} = M) -> M#{c := C + 1};
func(dec, #{status := update, c := C} = M) -> M#{c := C - 1};
func(_,   #{status := keep} = M)           -> M.

When dialyzing code using this function, we would like it to infer that the second argument has type #{status => update | keep, c => term()}. (Note that we cannot infer that c has type number(), because the third clause does not constrain c's value to be a number.) However, because the function will not crash if more keys are present in the second argument, that type cannot be inferred. Instead, the only type that can be inferred is map().

Moreover, even if the function is given a specification, such as this one from the example:

-spec func(Opt, M) -> #{'status' => S, 'c' => integer()} when
      Opt :: 'inc' | 'dec',
        M :: #{'status' => S, 'c' => integer()},
        S :: 'update' | 'keep'.

Dialyzer will be unable to find the error in a usage such as:

func(inc, #{c => 32}).

because the contract of the function allows one to omit the status key.

Another problem is related to the meaning of #{}. One would expect that this notation means "the empty map," but instead it means "any map". This not only makes writing map types more complex by adding unintuitive special cases, but also removes the most sane way of writing the singleton type of the empty map.

Proposed Syntax

We propose an extended syntax and semantics that:

• merges the two map type syntaxes, allowing both types to be used at the same time,
• removes the inconsistent #{} base case, and
• introduces a way to denote some keys as mandatory.

The syntax adds in map type specifications the := operator, which can be used instead of => to denote those keys that are mandatory. For example, func/2 above would likely be specified as follows, to denote that both keys are mandatory:

-spec func(Opt, M) -> M when
      Opt :: 'inc' | 'dec',
        M :: #{'status' := S, 'c' := integer()},
        S :: 'update' | 'keep'.

Of course, the old specification is still allowed and keeps its existing semantics.

In particular, if a map specification contains a pair K := V, then any map value must contain at least one key of type K in order to belong to the specification.

Further, we propose that types of keys and keys known beforehand may be mixed, and that earlier pairs take precedence over later. For example, the value #{a => "hej"} does not belong to the type #{atom() => integer(), any() => string()}, but does belong to the type #{integer() => integer(), any() => string()}

Lastly, we propose as a syntactic short-hand without any additional semantic meaning, that ... be allowed as a short-hand for any() => any(), when used as the last pair in a map type. This is very useful for Dialyzer, as a less cluttered way to write the type of any value that matches a map pattern. For example, consider func/2 above. Using the new syntax, an inferred success typing for this function would be:

-spec func(_, M) -> M when
      M :: #{status := update | keep, ...}.

Notable Special Cases

#{Forbidden => none(), ...}

Is any map, as long as it does not contain a key of type Forbidden. This form is allowed because of how useful it is internally to Dialyzer, and there is a desire to allow syntax for every type that Dialyzer can use internally, so that Dialyzer can express the fact that it has concluded that a key must not be present in a map without outputting types that are disallowed by the syntax.

Values of mandatory (:=) pairs, on the other hand, must not be none().

Preempting Discussions About the Semantics of the Old Syntax

Since the map EEP and documentation is vague about how the different syntaxes should be interpreted, there are other possible semantics that could be assigned to the old syntax. However, all of them are either ambiguous or are too weak for Dialyzer to make much use of. Thus it is insufficient to assign new semantics to the existing syntax.

Backward Compatibility Concerns

With the exception of #{}, existing 17.x-18.x syntax will continue to parse and will keep existing semantics. Modules using the new syntax will not be parsed by older compilers, but can use _=>_ instead of ... and => instead of := for a slightly more allowing type that does parse on older compilers. Although mixing keys known beforehand and types is not specified by the older syntax, it does parse, and no known tools are confused by it.

Since this proposal changes the semantics of the type #{}, old code using this syntax may result in unintended warnings from Dialyzer. The fix is very simple though: #{} can be exchanged for map(), its alias, in such code without breaking backwards compatibility.

Note that the function and type specification manual mentions that the map syntax is (still?) considered experimental.