Based on that classification a polymorphic type system is proposed that is based totally on extensionally defined polymorphic sets. Such sets may be defined locally and thus are of a locally known fixed size. Or they may be declared globally and then defined by explicit contributions given in different parts of the system. The latter form thus supports the open-world assumption.
Polymorphic sets may be built from other sets using the usual set operators union, intersection, and complement. These operators give a powerful means to define abstractions from other abstractions, allowing to express type classifications with exceptional elements. The empty set is the least element in the resulting lattice and its complement the greatest. Legality of assignments and subprogram calls is based on the subset relation between the type sets associated with the corresponding expressions. This legality relation between expressions is called "conformance".
Sets of subprograms provide for subprogram polymorphism, covering both the concepts of overloading and dynamic dispatching. Applying a subprogram set to a number of arguments the one most specifically applicable subprogram to work on the arguments is selected. Specificity between subprograms is defined by pointwise parameter and result types conformance. In case the argument expressions are of a polymorphic type, the selection in general has to take place at run-time. Because all arguments are considered for selection this is a form of multi-dispatching in the spirit of CLOS. Static checks are performed, however, to guarantee the absence of non-determinism (more than one most specifically applicable subprograms) and type errors (no applicable subprogram). The context of the application is also considered to constrain possible matching subprograms, comparable to overloading resolution in Ada.
The thesis investigates the interactions of polymorphic sets with second order type concepts, known as `genericity' or `type parametricity'. It is argued that an implicit style of type matching for calls to generic subprograms yields more freedom than an explicit style and the necessary rules for this implicit binding of type parameters are provided, which are based on the union and intersection of participating type sets.
These concepts are then used to define an experimental language called Hoopla. Considerations for the implementation of Hoopla are given, providing some sufficient conditions when global checks for subprogram sets can be avoided though keeping separate compilation.