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
andb
. If it contains a keya
, then it must be mapped to an integer value. Analogously forb
. -
#{binary() => integer()}
A map with 0 or more mappings, where all the keys are of type
binary()
and all values are of typeinteger()
.
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.
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, ...}.
#{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()
.
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.
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.