Currently, we allow a user to create maps (dictionary data structures) using the NV syntax createDict v and then updating the map using m[key := e] syntax.
For the special case of a map where the type of values is bool, i.e. a set, we provide additional syntactic sugar { e1, e2, ..., en } that (internally) unrolls into (createDict false)[e1 := true][e2 := true]...[en := true] and allows a user to initialize a set far more quickly.
It seems useful to implement this functionality for maps which use other types of values as well. Notably, there is a syntax used when printing maps that cannot be used to create them: { x1 |-> y1\nx2 |-> y2\nx3 |-> y3 }.
Proposal
This issue proposes that we add the print formatting of maps as an additional syntactic expression that internally unrolls into a map creation followed by a series of updates, as in the case of sets.
In order to handle the fact that the current print formatting does not specify the default value of the map to use when the given value is not found, this issue proposes a modification to the syntax for printing maps and for creating maps:
Printing maps should include the default value v as an additional key-value pair _ |-> v.
Creating maps using the sugared syntax requires a _ |-> v or else parsing will fail.
Changing the syntax for separating key-value pairs when printing maps: instead of a newline, use a semicolon. a |-> b\nc |->d becomes a |-> b; c |-> d.
Benefits
Unifies the printed representation of maps with the actual syntax necessary to create them. With this change, I believe any printed NV expression is also syntactically valid.
Provides a shorthand for users to initialize maps in the same vein as set initialization.
Drawbacks
None I can really think of: it's some amount of work to actually add. :laughing:
Considerations
|-> may be an inelegant/overly-noisy separator to use between the key-value pair, although it resembles the LaTeX \mapsto. : is probably undesirable since we use it for type annotation. We could use :=, but I personally feel that |-> is distinct enough and still saves the user a keystroke over the current representation.
Introduction and Current Situation
Currently, we allow a user to create maps (dictionary data structures) using the NV syntax
createDict vand then updating the map usingm[key := e]syntax. For the special case of a map where the type of values isbool, i.e. a set, we provide additional syntactic sugar{ e1, e2, ..., en }that (internally) unrolls into(createDict false)[e1 := true][e2 := true]...[en := true]and allows a user to initialize a set far more quickly. It seems useful to implement this functionality for maps which use other types of values as well. Notably, there is a syntax used when printing maps that cannot be used to create them:{ x1 |-> y1\nx2 |-> y2\nx3 |-> y3 }.Proposal
This issue proposes that we add the print formatting of maps as an additional syntactic expression that internally unrolls into a map creation followed by a series of updates, as in the case of sets. In order to handle the fact that the current print formatting does not specify the default value of the map to use when the given value is not found, this issue proposes a modification to the syntax for printing maps and for creating maps:
_ |-> v._ |-> vor else parsing will fail.a |-> b\nc |->dbecomesa |-> b; c |-> d.Benefits
Drawbacks
Considerations
|->may be an inelegant/overly-noisy separator to use between the key-value pair, although it resembles the LaTeX\mapsto.:is probably undesirable since we use it for type annotation. We could use:=, but I personally feel that|->is distinct enough and still saves the user a keystroke over the current representation.