Chapter 7. Modularity

Table of Contents
Types as a Form of Specification
Static and Dynamic ATS Files
Generic Template Implementation
Specific Template Implementation
Abstract Types
Example: A Package for Rationals
Example: A Functorial Package for Rationals

Generally speaking, modularity in programming means to organize programs in a modular fashion so that they each can be constructed in a relatively isolated manner and then be combined to function coherently. I will introduce in this section some features in ATS that are largely designed to facilitate program organization.

The code employed for illustration in this chapter plus some additional code for testing is available on-line.

Types as a Form of Specification

The interface for a function or value specifies a type that any implementation of the function or value should possess. For instance, the following code defines a function fact for computing the factorial of a given integer:

fun fact (x: int): int = if x > 0 then x * fact (x-1) else 1

It is also possible to first declare an interface for fact as follows:

extern fun fact (x: int): int

where extern is a keyword in ATS that initiates the declaration of an interface. Alternative ways to declare an interface for fact are given as follows:

extern fun fact : (int) -> int extern val fact : (int) -> int

If fact is declared to be a function, then it is required to be applied when occurring in code. If it is declared to be a value, there is no such a restriction.

A function interface can be considered as a form of specification. For instance, the above interface for fact specifies that fact is a function that takes one argument required to be an integer and returns a value guaranteed to be an integer. What is so special about this form of specification is that it is formally enforced in ATS through typechecking: Any well-typed implementation of fact in ATS must possess the interface declared for it. Of course, this interface for fact is not a precise specification as there are (infinitely) many functions that can be given the same interface. This kind of imprecision can, however, be reduced or even eliminated, sometimes. After dependent types are introduced, I will present an interface for fact such that any implementation of the interface is guaranteed to implement precisely the factorial function as is defined by the following two equations:

An implementation for fact as the following one can be given at any point where the declared interface for fact is accessible:

implement fact (x) = if x > 0 then x * fact (x-1) else 1

The keyword implement is for initiating an implementation of a function or value whose interface is already declared. It is fairly common to see the following style of coding, usually, by a beginning ATS programmer:

implement fact (x: int): int = if x > 0 then x * fact (x-1) else 1

While this implementation can pass typechecking, it is nonetheless of a poor style: The types provided by the programmer for the argument and the result of fact are redundant as they can be automatically synthesized by the typechecker.

As an example of an interface for a value, fact10 is declared as follows to be a value of the type int:

extern val fact10 : int

The following implementation for fact10 can be given at any point where the declared interface for fact10 is accessible:

implement fact10 = fact (10)

As another example, the following code declares an interface for a polymorphic function named swap_boxed:

extern fun swap_boxed{a,b:type} (xy: (a, b)): (b, a)

Note that both type variables a and b are boxed. An implementation for swap_boxed is given as follows:

implement swap_boxed{a,b} (xy) = (xy.1, xy.0)

The syntax {a,b} is for passing static arguments a and b to swap_boxed simultaneously. As neither a nor b is actually used in the body of swap_boxed, it is allowed to drop {a,b} in this case.

As yet another example, the following code declares an interface for a function template named swap_tmplt:

extern fun{a,b:t@ype} swap_tmplt (xy: (a, b)): (b, a)

Note that both type variables a and b are of the sort t@ype, indicating that they can be of any size. An implementation for swap_tmplt is given as follows:

implement{a,b} swap_tmplt (xy) = (xy.1, xy.0)

It is a standard practice for a programmer to first design interfaces for the functions to be supported in a package before actually implementing any of these functions. When such interfaces are available, application programs can be constructed to test whether the interface design makes sense or is convenient for practical use. Please remember that a superb implementation of a poor design cannot make the design any better. Therefore, testing a design before actually implementing it is often of vital importance. This is especially true if the involved design is complex.