Arrays

The array construct of classical languages is simply a special case of the map type constructor provided by the proposed syntax. Thus, the classical declaration

A : array 1...10 of Integer;

would be written as

A : map from {1...10} to Integer

and should be viewed as syntactic sugar for the function

$a$ : {} $\to$ { Integer}

Furthermore, A should be understood as $a()$ and A[1] as $(a())(1)$. Finally, assignments to elements of A should be viewed as incremental redefinitions of $a$.

Note, however, that the construction of generalized array operators, makes it necessary to specify that type expressions may contain free variables in certain circumstances. The reason for this is that types Vector10 and Vector20, where

Vector10 = maps from {0...9} to Integer
Vector20 = maps from {0...19} to Integer

represent disjoint sets of values, and hence operator Sum20, where

Sum20 : Vector20 $\to$ Integer

may not be applied to any array of type Vector10.

Using free variables instead, one may have

Vector = maps from {L...U} to Integer
Sum : Vector $\to$ Integer

where type Vector is understood to be the set

$$_{{L&sp; ≤&sp; U}L,&sp; U&sp; ∈&sp; Integer} {f&sp; |&sp; f : {L, &ldots;, U} → Integer}

The above definition would allow Sum to be applied to any map from a single domain, consisting of a contiguous range of integers, to Integer. Furthermore, by specifying that L and U are parameters of Sum, and that L and U must automatically be set to integer values representing the lower bound and upper bound of the first parameter, it becomes possible for Sum to determine the index range of an actual parameter.