Forked from margnus1/map_spec_extension_proposal.md
Last active
April 13, 2016 20:15
Revisions
-
kostis revised this gist
Mar 12, 2016 . 1 changed file with 2 additions and 4 deletions.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -21,8 +21,7 @@ Consider the following example from the Maps EEP: 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()`. @@ -69,8 +68,7 @@ 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 -
kostis revised this gist
Mar 11, 2016 . 1 changed file with 21 additions and 20 deletions.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -3,7 +3,7 @@ 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()}` @@ -24,18 +24,17 @@ Consider the following example from the Maps EEP: When dialyzing code using this function, we would like it to infer that the second argument has type `#{status => update | keep, c => term()}`. 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}). @@ -44,25 +43,25 @@ 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 @@ -75,19 +74,19 @@ string()}`, but does belong to the type `#{integer() => integer(), any() => stri 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 @@ -99,7 +98,7 @@ 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. @@ -114,5 +113,7 @@ 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](http://erlang.org/doc/reference_manual/typespec.html) mentions that the map syntax is (still?) considered experimental. -
kostis revised this gist
Mar 11, 2016 . 1 changed file with 41 additions and 45 deletions.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -1,91 +1,87 @@ # Current Syntax Existing map specification syntax, as was introduced in 17.0, allows the following different syntaxes: - `map()` or `#{}`: 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()`. # 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()}`. 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 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) -> #{'status' := S, 'c' := integer()} when Opt :: 'inc' | 'dec', M :: #{'status' := S, 'c' := integer()}, S :: 'update' | 'keep'. Of course, the old specification are still allowed and keep 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(_, #{status := update | keep, ...}) -> #{status := update | keep, ...}. ## Notable Special Cases @@ -109,14 +105,14 @@ 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()` in such code without breaking backwards compatibility. -
margnus1 revised this gist
Mar 7, 2016 . 1 changed file with 26 additions and 24 deletions.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -1,11 +1,9 @@ # Current Syntax Existing map specification syntax, as was introduced with R17, allows four different syntaxes: `map()` or `#{}`: the type of any map. #{a => integer(), b => list()} @@ -46,11 +44,17 @@ Dialyzer will be unable to find the error in a usage such as because the contract of the function allows you to omit the `status` key. Finally, `#{}` appears to be a base-case for the first syntax, which would have it mean "only the empty map," but instead it means "any map," not only making writing map types more complex by adding unintuitive special cases, but also removing the most sane way of writing the type of the empty map. # Proposed Syntax 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 removing the inconsistent `#{}` base case and 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 @@ -90,31 +94,29 @@ typing for this function would be 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 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. Since this proposal changes the semantics of the type `#{}`, old code using this syntax will experience breaking change, and receive unintended warnings after this change, luckily, this syntax can be exchanged for `map()` in such code without breaking backwards compatibility. -
margnus1 revised this gist
Feb 29, 2016 . 1 changed file with 4 additions and 0 deletions.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -64,6 +64,10 @@ likely be specified as follows, to make both keys mandatory: Of course, the old specification would still be allowed and keep 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, 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() => -
margnus1 created this gist
Feb 29, 2016 .There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -0,0 +1,116 @@ # Current Syntax 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()`. # 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 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. # Proposed Syntax 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, ...}. ## 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 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()`. ## Preempting Discussions About the Semantics of the Old Syntax 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. # Backward Compatibility Concerns 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.