map ≝ {any→any|}

Simply put, a map is a relation between keys and values. More formally, a map is an immutable, finite, unordered, indexable, directed, one-to-one function from a domain of distinct, homogeneous keys to a codomain of homogeneous values. Each association from key to value is a binding. The number of bindings is the cardinality of the map. A map is therefore a discrete mathematical function. Breaking this down:

• Immutable means that the composition of a map is not subject to change. No operations are, or can be, defined to modify a map in any way; only operations that derive new maps from existing maps are expressible.
• Finite means that the cardinality of a map is never the value ∞. To store a map in memory requires space proportional to its cardinality, and memory is clearly always finite. Additional limits to the practical cardinality of maps may be imposed by the implementation. Given that m is a map, then |m| is the size of m. The method for sizing is "`|_`|".
• Unordered means that the bindings of a map do not occur in any particular order. Any two maps with the same bindings are therefore equal.
• Indexable means that a value of the codomain can be accessed by supplying a key that is associated with that value by some binding. Given that m is a map and k is a key of the map's domain, then m[k] denotes the value of the codomain that is bound to k. The method for subscripting is "_[_]".
• Directed means that obtaining a value of the codomain given a corresponding key efficiently supplies a unique answer. But many keys may be bound to the same value, and determining which keys are bound to a particular value is not necessarily efficient.
• One-to-one means that each key of the domain is associated with exactly one value of the codomain.
• Distinct means that a key uniquely identifies a binding of a map. Any particular value is either a key of a map or it is not.
• Homogeneous means that the keys of the domain conform to a single most general type and the values of the codomain conform to a single most general type. These types need not be equal.

A literal map is expressed as a left curly bracket { (U+007B), then a comma-separated list of bindings, and finally a right curly bracket } (U+007D). A literal binding is expressed as a key, then a rightwards arrow → (U+2192), and finally a value. Examples of maps include {"United States"→"Washington, D.C.", "Mongolia"→"Ulaanbaatar", "Tanzania"→"Dodoma"}, {1→<1>, 2→<1, 4>, 3→<1, 4, 9>}, and {4→"四", 5→"五", 6→"六", 7→"七"}. The empty map is written as {}.

The elements of a map need not be known statically. Maps are constructed with the macro "{«_→_‡,»}"; there is no special built-in syntax for constructing maps. When the compiler can infer an instance type for each argument expression of a particular send of this message, then the semantic restriction is able to strengthen the result to an instance type, thereby according it the same force as a literal understood primitively by the compiler.

The map type specifies three parameters for completion:

• The key type specifies a type that includes every key of the domain. For example, a map type whose key type is string has as instances the maps {"Billy"→5}, {"Jane"→"enaJ", "Kylie"→"eilyK"}, and {}. The method "_'s⁇key type" answers the key type of a map type.
• The value type specifies a type that includes every value of the codomain. For example, a map type whose value type is function has as instances the maps {"="→[a : integer, b : integer | a=b], "≥"→[a : integer, b : integer | a ≥ b]} and {"Avail"→[Print: "Just shut up and use it.\n";]}. The method "_'s⁇value type" answers the value type of a map type.
• The cardinality restriction is an integral type that specifies the range of sizes that describe instances. If the cardinality restriction is [0..2], then only a map whose cardinality is 0, 1, or 2 is an instance. The method "`|`|_`|`|", read as sizes of, answers the cardinality restriction of a map type. The floor operation, ⎣_⎦, answers the lower bound of a map type's cardinality restriction. The ceiling operation, ⎡_⎤, answers the upper bound of a map type's cardinality restriction.

The primitive map type constructor is "{_→_|_}". It accepts the key type, value type, and cardinality restriction, respectively. This method supports the most general type construction scenario, that of three statically unknown type completion arguments. Most type construction is done by the compiler during execution of type annotations, however, so typically most or all of the map type completion arguments will be known at compile-time. For these more common situations, the system library provides the following convenience methods:

• The method "{_→_|_.._}" accepts the key type, value type, the lower bound of the cardinality restriction, and the upper bound of the cardinality restriction, respectively. To determine the cardinality restriction, take the specified lower and upper bounds — lower and upper, respectively, in the following expression — and compute the type [lower..upper+1). Canonization of integral ranges causes the specified upper bound to be considered inclusive if it is finite and exclusive if it is infinite.
  /* Here's a map type with an inclusive upper bound on its cardinality * restriction. */ mapType ::= {integer→double|2..4}; Assert: mapType's key type = integer; Assert: mapType's value type = double; Assert: ||mapType|| = [2..4]; /* And here's one with an exclusive upper bound. */ Assert: ||{string→string|13..∞}|| = [13..∞); /* Here are some example instances of "mapType". */ Assert: {2→2.0, 503→503.0} ∈ mapType; Assert: {-1→1.0, -4→16.0, -7→49.0} ∈ mapType; Assert: {3→-3.0, 5→-5.0, 8→-8.0, 13→-13.0} ∈ mapType; /* And here is an example non-instance (because it's too large). */ Assert: {0→0.0, 1→1.0, 2→2.0, 3→3.0, 4→4.0, 5→5.0} ∉ mapType;
• The method "{_→_|_..}" accepts the key type, the value type, and the lower bound of the cardinality restriction, respectively. To determine the cardinality restriction, take the specified lower bound, lower, and compute the type [lower..∞).
  mapType ::= {string→string|1..}; Assert: mapType's key type = string; Assert: mapType's value type = string; Assert: ||mapType|| = [1..∞); /* Here are some example instances of "mapType". */ Assert: {"dengue"→"kidingapopo"} ∈ mapType; Assert: {"Borr"→"Bestla", "Thor"→"Sif", "Njörðr"→"Skaði", "Óðinn"→"Frigg"} ∈ mapType;
• The method "{_→_|.._}" accepts the key type, value type, and the upper bound of the cardinality restriction, respectively. To determine the cardinality restriction, take the specified upper bound, upper, and compute the type [0..upper+1).
  mapType ::= {set→integer|..2}; Assert: mapType's key type = set; Assert: mapType's value type = integer; Assert: ||mapType|| = [0..2]; /* Here are some example instances of "mapType". */ Assert: {} ∈ mapType; Assert: {{1, "fish", 2}→3} ∈ mapType; Assert: {∅→0, {"megaphone"}→1} ∈ mapType;
• The method "{_→_|_}" is overridden to accept, respectively, the key type, the value type, and a whole number that specifies the exact size of instances. To determine the cardinality restriction, take the argument, exact, and compute the type [exact..exact].
  mapType ::= {[0..1]→[0..1]|1}; Assert: mapType's key type = [0..1]; Assert: mapType's value type = [0..1]; Assert: ||mapType|| = [1..1]; /* Here are the four instances of "mapType". */ Assert: {0→0} ∈ mapType; Assert: {0→1} ∈ mapType; Assert: {1→0} ∈ mapType; Assert: {1→0} ∈ mapType;
• The method "{_→_|}" accepts the key type and value type, respectively. The cardinality restriction is [0..∞).
  mapType ::= {character→code point|}; Assert: mapType's key type = character; Assert: mapType's value type = character; Assert: ||mapType|| = [0..∞); /* Here are some example instances of "mapType". */ Assert: {¢a→97, ¢b→98, ¢c→99} ∈ mapType; Assert: {¢∪→8746, ¢∩→8745} ∈ mapType; Assert: {¢1→49, ¢2→50, ¢3→51, ¢4→52, ¢5→53} ∈ mapType;

A map type is covariant by key type, value type, and cardinality restriction.