4.9.7 Map

A map models a total function from a domain to a co-domain by a record whose arity is the domain, and whose type at all fields is the co-domain. The domain must be a finite domain of constants, while the co-domain can have any type.

This is a type synonym for the Record type:

     field_1:type,...,field_n:type

where field_1,...,field_n are the elements of the domain of the function, and type is the type of the co-domain.

4.9.7.1 Example

Here is an example map type definition from domain ref("domain") to co-domain ref("codomain"):

     deftype "map" vec(ref("domain") ref("codomain"))