Existing map specification syntax, as was introduced with R17, allows three different syntaxes:
map()
The type of any map.
#{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().
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 to be of type #{status => update | keep, c => _} as a value.
However, because the function will not crash if more keys are present in the
second argument, that type cannot be used. The only syntactically valid type
that could possibly be inferred is map(), as any other type would preclude
maps that do not cause func/2 to crash.
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 you to omit the status key.
Instead, I propose an extended syntax and semantics that merges the two map type syntaxes, allowing both types to be used at the same time, as well as introducing a way to denote some keys as "mandatory", that may not be omitted.
I propose that in map type specifications, the := operator be used instead of
=> to denote those keys that are mandatory. For example, func/2 above would
likely be specified as follows, to make both keys mandatory:
-spec func(Opt, M) -> #{ 'status' := S, 'c' := integer() } when
Opt :: 'inc' | 'dec',
M :: #{ 'status' := S, 'c' := integer() },
S :: 'update' | 'keep'.
Of course, the old specification would still be allowed and keep existing semantics.
Further, I propose that types of keys and keys known before hand 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 #{any() => string()}
Lastly, I 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 optimal success
typing for this function would be
-spec func(_, #{status := update | keep, ...})
-> #{status := update | keep, ...}.
#{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
the introduction of a function specification does not weaken the analysis
Dialyzer can do due to the syntax being less expressive.
Values of mandatory (:=) pairs, on the other hand, must not be none().
Since the map EEP 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.
Existing R17-R18 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 before hand
and types is not specified by the older syntax, it does parse, and no known
tools are confused by it.
One concern is that, even though the old syntax leaves the semantics of the type
#{} undefined, the fact that Dialyzer from R17 and R18 formats the type
map() as #{} might have fooled users into using #{} to mean map() (any
map). With this syntax change, the type #{} becomes well defined as the type
containing only a single value, #{}. Thus, any code using the type #{} in
this way will get unintended Dialyzer warnings.