There is probably no area in which the advantage of using Ada as a specification language for SETL is more clear than in the area of types. First of all, let me make the general observation that the design of types requires a much higher degree of care and professional experience than virtually any other aspect of program design. This has been evident time and again in the parade of versions of the Java API, the C++ standard library, and even some of the Ada packages that have appeared over the years, especially generics.
Types play a pivotal role in any large system. They are at the core, and much depends on them--they are in many ways the foundation, and I think their centrality makes it fair to consider their design to be in the realm of systems programming rather than applications programming.
SETL, on the other hand, belongs very much in the sphere of applications and, as I have tried to illustrate in this dissertation, is best suited to small programs. Furthermore, its maps and even its tuples serve, however informally, the main purpose of types, which is to package data objects. On their own, maps and tuples do not support formalized abstraction, but the fact that they are values makes them very convenient packets to pass among the routines which do embody an abstraction.
The foregoing helps to explain why the absence of a type system in SETL has been less uncomfortable than it would be in a language like Ada, which aims to support programming in the large at both the systems and the applications level. We see a similar phenomenon in textbooks on algorithms, where the focus is on mechanisms rather than on organizing large bodies of code. Variables are often not even declared, since (for example) seeing A(i) immediately tells us that A is a map, perhaps an array, the presence of and R.a indicates that R is an object with an attribute a, perhaps a record. The genericity in expressions like A(i) extends also to scalars, where in fact it often does not matter what kind of number x is, or even whether x is a number at all. The reader can then take an appropriately abstract view of x until x is seen to be involved in arithmetic or some other expression requiring more specificity.
Still, it is unfortunate that SETL follows the tradition of textbooks to the point of making it difficult to manage a program of significant size, and a non-intrusive type system for SETL would be welcome.
To me, there are two main aspects to how this might be done. One is that type declarations, even when they become available, should remain optional, but it is very important that the compiler and the human reader of a given program unit P come to an understanding about P right from the outset: if P is marked strong, then every variable and formal parameter in P must be declared, but if P is marked weak (the default), then any undeclared variable is implicitly var, just as in the current SETL. Programmers writing new code would of course be gently encouraged to declare their program units strong to gain the advantages of type checking and possible run-time efficiency improvements, except in cases where this would add more clutter than perspicuity.
The second aspect of non-intrusiveness is that the introduction of a SETL type system should not rob the language of its essential simplicity. This is why I have been at some pains to point out that the design of ``core'' types is a challenging systems programming activity, and why I began this section by asserting that Ada has advantages as a specification language for SETL. I think the extreme position of introducing new types into a SETL program only by slipping into Ada or very Ada-like declarative forms is defensible, and that the ideal approach is not far from that extreme.
However, I feel that SETL should at least acquire some simple forms for defining and extending record types, and for specifying subtypes via Ada-like constraints. These forms should have obvious transliterations into Ada. It is difficult to say more at this stage, except that we should be strictly guided by need in order to avoid inventing myriad declarative forms for SETL of marginal utility. A good starting point is perhaps to add nothing more to SETL than the ability to state that a given type named T is described by a piece of Ada code somewhere. Whether T is tagged (perhaps all types visible to SETL should be), limited private (perhaps no types visible to SETL should be), etc., and what operations on T are described by Ada routines, could all conceivably be specified in pure Ada. If T meets the requirements of a SETL type, which could be quite restrictive and stereotyped, doubtless including some uncheckable and even unstated semantic promises, then T can be admitted to visibility at the SETL level. There are some operations which apply to all SETL types (like the type operator), and undeclared SETL variables will always be able to change their types dynamically, notwithstanding the fact that part of the purpose of a type system will be to help the programmer constrain and group such chameleons appropriately. Dynamic dispatching to routines with fully type-constrained formals should certainly be available. The upshot of the need for these essential features in SETL variables is that they should all derive from some base ADT in Ada that encapsulates the descriptor, or stub, together with the operations that all SETL variables inherit.
There are many issues surrounding types that have not been touched on here, such as (1) the syntax of typed variable declarations in SETL, (2) whether type and variable declarations need to remain segregated from other statements, or can be integrated as in Algol 68 and C++, (3) scopes and interactions with package structure, (4) child packages, (5) generics, (6) inheritance of multiple abstract types, (7) dynamic dispatching based on multiple argument types, (8) communication of typed values between programs, and (9) the possibility of representational ``hints'' along the lines of the old SETL repr clauses.