Type-Oriented Logic Meta Programming

This is short summary of the story of my Ph.D. dissertation. If you find it interesting, you can download the full version (pdf). This summary is also availabe in PDF-format (PDF file has a short bibliography).

Thesis

The dissertation shows that undecidable and ambiguous type systems have useful applications and should therefore be considered viable options for future statically typed object-oriented\footnote{This statement can probably be made about static type systems in general. This dissertation however focuses of object-oriented languages.} languages.

Traditionally, type systems have been included into programming languages for the following reasons [Madsen:90]:

• documentation: Static types improve the readability of programs.
• robustness: Detection of ``type errors''.
• efficiency: Optimizations based on static type knowledge.

The aforementioned uses are passive in the sense that types have mostly a descriptive nature. This makes them great as documentation. The type checker verifies whether the description is a consistent one and this increases robustness by eliminating type errors. Optimizers also make use of the descriptive nature of types to perform optimizations.

We want to draw attention in this dissertation to the potential of ``actively'' using static types, writing real programs that manipulate types: consult them, construct them, or make decisions regarding interfaces or internal representations of classes. In short, we want to draw attention to the potential of active manipulation of types by real ``type programs'', expressed with a real, Turing-complete, type-programming language. It is in this active type manipulation that lies the currently unharvested potential which makes undecidable and ambiguous type systems potentially useful.

Dissertation

To prove our thesis we implemented a system which offers a full-fledged logic programming language with which types can be constructed, consulted and implemented. This approach is highly reminiscent of and inspired by the flavor of instance declarations for type and constructor classes [Kaes:88,Wadler:89,Jones:93c,Jones:94c,Odersky:95] in the functional languages Gofer [Jones:95b] and Haskell [Peterson:97].

Because of limited resources we have been forced to take a less than perfect approach. The system we implemented is not a real type system in the true sense of the word since it does no type checking of its own. Type systems for object-oriented languages being very complicated artifacts both theoretically and implementation wise, this was not a feasible option to us. Instead, our system generates Java code and leaves type checking to the Java compiler. Potential type errors are therefore only detected in as far as the generated output code violates the Java typing rules. Clearly this is not what one wants for a production level environment. However, since the added potential of having a Turing-complete type language is in active type manipulation rather than in the type-checking aspect of the system, this is sufficient to prove our point.

The dissertation provides several examples that illustrate the usefulness of having a real, Turing complete, type-programming language. These examples show how type-oriented meta programming complements the expressiveness of the base programming language. Amongst others, we discuss how type-oriented logic meta programming is potentially useful to support aspect-oriented programming.