Update documentation about map types

Summary: Update documentation to reflect recent changes to map types.

Reviewed By: ilya-klyuchnikov

Differential Revision: D65268381

fbshipit-source-id: 8ef19fd7198d2a56b60e2b658d85b416b6593125

docs/reference/errors.md

@@ -108,29 +108,6 @@ when a function is called with the wrong argument type:
 ```
 
 
-#### Shapes and maps
-
-Another kind of type error occurs when a dictionary map is used where a
-shape map is expected:
-
-```Erlang
--spec test_neg(atom()) -> #{a := v}.
-    test_neg(Atom) -> #{Atom => v}.
-
-% #{..}.
-% Expression has type:   dict map #D{atom() => v}
-% Context expected type: shape map #S{'a' := v}
-```
-
-In this case, either the return type must be modified, or the argument must be
-pattern matched to ensure that `Atom = a`.
-
-For best practices for writing specs, see writing specs.
-For more information about the type system, including dynamic(), term(),
-and shapes, see [Syntax of types and specs in eqWAlizer](./types.md)
-and [Subtyping in eqWAlizer](./subtyping.md).
-
-
 ### not_enough_info_to_branch
 
 This error happens when there is not enough information to know which sub-spec
@@ -172,52 +149,6 @@ test_neg() ->
 ```
 
 
-### fun_in_overload_arg
-
-A fun cannot be used as an argument to an overloaded function. This restriction
-enables eqWAlizer to have predictable behavior for users when type-checking the
-application and calculating which overloaded sub-spec to use.
-
-Example:
-```Erlang
--spec test_bar1() -> b.
-test_bar1() ->
-    Res = bar(fun(a) -> a end),
-    Res.
-
-% bar(fun). Lambdas in overloaded calls are not supported
-```
-
-
-### undefined_key
-
-This error occurs when using `:=` to update a key in a map, but the map is not
-guaranteed to have the key.
-
-Example using a shape map:
-```Erlang
--spec test_neg(#{a := v }) -> nok.
-test_neg(M) ->
-    M#{z := v}, % Error
-    nok.
-
-% M. Undef key `z`. Type: #S{a := 'v'}
-```
-
-- To fix this error when the property is required, add the required property to the spec: #{a := v, z:= v}
-- To fix this error when the property is optional, use an optional property update: M#{z => v}
-
-Example using a dict map:
-```Erlang
--spec test_neg(#{atom() => v }) -> nok.
-test_neg(M) ->
-    M#{z := v}, % Error
-    nok.
-```
-
-In dict maps, all properties are optional. Always use optional property updates with dict maps: M#{z => v}
-
-
 ### undefined_field
 
 This error occurs when attempting to create a record with a field that does not exist.
@@ -419,7 +350,10 @@ or write the type directly, without using constraint syntax:
 
 ### bad_map_key
 
-This error indicates that a property of a map type is marked as required (`:=`)
+This error indicates that a property of a map type is invalid, which can occur for
+two reasons.
+
+First, a property may be marked as required (`:=`)
 in a place where only an optional property would make sense (`=>`). For example,
 the following code says that `atom()` is required. But code calling the function
 cannot know which atom is required, so the information in the spec is not
@@ -433,10 +367,22 @@ actionable:
 % Bad map key
 ```
 
-The fix is to either:
+Second, the map may contain several "default" associations, i.e., associations
+that are not singleton types (such as atoms and tuples of atoms). An example is the
+following:
+
+```Erlang
+-spec test(_) -> #{
+    atom() => pid(),
+    integer() => binary()       % Error
+}.
+
+% Bad map key
+```
 
-- specify an optional property instead of an optional property: `atom() => pid()`;
-- use a specific atom, which would make this map a shape map, for which required keys are allowed: `#{pid := pid()}`.
+While it may be sound in some examples such as the one above, in the general case,
+the default keys (here `atom()` and `integer()`) may overlap, leading to confusing
+signal. As such, only one default association is allowed per map.
 
 
 ### dyn_remote_fun

docs/reference/subtyping.md

@@ -93,12 +93,12 @@ on the left hand side of a function type in a type alias. For example, the type
 since it is not covariant in `X`.
 
 
-### Shapes and dictionaries
+### Maps
 
-In eqWAlizer, the fields of a shape must match the fields specified in its type, with some
+In eqWAlizer, the fields of a map must match the fields specified in its type, with some
 exceptions regarding optional fields. For example, the following function
-does not type-check, since the shape `M` has two fields `a` and `b`, and we expect
-the function to return a shape with only a single field `a`:
+does not type-check, since the map `M` has two fields `a` and `b`, and we expect
+the function to return a map with only a single field `a`:
 ```erlang
 -spec forget_key(#{a := term(), b := number()}) -> #{a := term()}.
 forget_key(M) -> M.
@@ -115,12 +115,11 @@ function type-checks:
 maybe_keys(M) -> M.
 ```
 
-Shapes are automatically upcast to dictionaries when needed, or when eqWAlizer
-is unable to deduce precise enough information. For example, given a shape `M`
-`#S{a := number()}`, if one writes `maps:put(A, 42, M)` where `A` is of type
-`atom()` but the precise atom cannot be known, the result will be a dictionary
-of type `#D{atom() => number()}`.
-
-This also means that shapes can be used when dictionaries are expected. For
-example, a shape of type `#S{a := integer(), b := float()}` can be used as
-a dictionary of type `#D{atom() => number()}`.
+Is is also possible to "forget" any number of keys by introducing a default association
+containing them:
+```erlang
+-spec forget_keys(#{a := term(), b := atom(), c => number()}) -> #{a := term(), atom() => atom() | number()}.
+forget_keys(M) -> M.
+```
+Here, the default association `atom() => atom() | number()` supersedes both associations `b := atom()`
+and `c => number()`, making the types compatible.

docs/reference/types.md

@@ -21,45 +21,34 @@ All numeric types (`integer()`, `float()`, integer ranges, `byte()`, etc)
 are all converted into type `number()` before type-checking.
 
 
-### Maps: shapes and dictionaries
+### Maps
 
-To make eqWAlizer more expressive, Erlang maps are separated into two
-categories: shapes and dictionaries.
+Map types in eqWAlizer contain two parts: a set of associations whose keys are
+statically-defined singleton types, and a default association. Both are optional:
+a map type can contain one or the other, both, or none (in which case it will just be `#{}`).
 
-#### Shapes
+The first part is composed of keys that are statically-defined atoms or nested tuples
+of such atoms. For example, the atom `a`, and the tuple `{a, {b, c}}` are such keys.
+Corresponding associations can be marked as optional `=>` or mandatory `:=`, for example,
+`#{a => atom(), {a, {b, c}} := binary()}`.
 
-Shapes are maps whose keys are all explicitly defined atoms. For example,
-the type `-type my_map :: #{a => term(), b := number()}` is interpreted by eqWAlizer
-as the type of shapes with an optional association `a => term()` and a
-mandatory association `b := number()`. To emphasize the fact that it is
-understood as a shape, eqWAlizer will report this type as
-`#S{a => term(), b := number()}`.
-
-EqWAlizer attempts to track the type of shapes as precisely as possible on a
-best-effort basis, with several OTP functions having a custom implementation
-in eqWAlizer to produce more accurate types. For example, given a shape `M` of
-type `my_map` above, `maps:put(c, 42, M)` will return a shape of type
-`#S{a => term(), b := number(), c := number()}`.
-
-
-#### Dictionaries
-
-A map whose keys are not all explicitly defined atoms is a dictionary.
-If eqWAlizer is not able to precisely deduce the atoms associated to the
-keys of a map, then it attempts to understand it as a dictionary.
-A dictionary in eqWAlizer is a map containing exactly one optional association,
-from a type to another type, such as `#D{atom() => number()}` for the type
-of dictionaries mapping atoms to numbers. EqWAlizer differentiates dictionaries
-from shapes by printing them using `#D` instead of `#S`.
+The second part is the so-called "default association", which is necessarily marked as
+optional, and can contain any key/value combination, e.g. `#{atom() => binary()}`.
+For complexity reasons and to preserve good signal, only one such association is allowed
+per map type. The default association will have the least precedence when understanding
+a map type. For example, the type `#{a => integer(), atom() => binary()}` stands for
+maps that optionally associate the atom `a` to an integer, and any other atom to a
+binary.
 
 Note that the Erlang syntax allows for some ambiguous map types to be defined.
 For example, it is possible to define maps with mandatory associations such as
 `#{atom() := number()}`, in which case it is not clear whether such a map
 must contain a mapping *for every* atomic key, or *at least one* mapping with
-an atomic key. Similarly, one can define heterogeneous maps such as
-`#{a => binary(), atom() => atom()}`, in which case it is not clear what can
-be stated about a map such as `#{a => ok}`. To avoid such questions, eqWAlizer
-interprets all such maps as the dictionary `#D{dynamic() => dynamic()}`.
+an atomic key. Similarly, one can define maps with multiple overlapping default
+associations `#{term() => binary(), atom() => atom()}`, in which case the precedence
+of associations is unclear. To avoid such questions, eqWAlizer
+interprets all such maps as the map type `#{dynamic() => dynamic()}`, issuing
+an error in the process.
 
 
 ### List types