A generator for type checkers

Abstract

Compiler-compilers are tools that generate substitutes for hand-written compiler components from high-level formal specifications. Such tools exist for lexical, syntactic and semantic analysis, optimizers and code generation. The established benefits are reduced development time and increased confidence in the correctness of the resulting software.

This thesis presents a generator for type checkers. Given a description of the type system by typing rules, the generator yields a type checker that constructs proofs using the typing rules. Unlike earlier approaches, we derive suitable notions of proof and typing rule from an analysis of type systems and from corresponding constructs in mathematical proof theory. The approach thus respects the structure and intention of the typing rules, rather than expressing the rules in some pre-existing formalism.

The given applications comprise type checkers for imperative, object-oriented and functional languages, including ML type inference. The typing rules for these checkers directly represent those found in the literature. They naturally describe the typing of single language constructs and they can be re-used in different checkers.

We use the generator to develop the language Saga for generic programming. Generic programming has become a standard approach to creating reusable and reliable software, particularly through the wide-spread use of the C++ Standard Template Library (STL). Existing C++ compilers cannot type-check generic algorithms before instances are generated, hence errors manifest themselves only when the algorithms are used. Saga overcomes this problem by a novel language design that enables generic algorithms as found in the C++ STL to be type-checked such that the correctness requirements stated in algorithm interfaces are obeyed and instantiation never fails. It therefore turns the aims of the earlier proposal SuchThat into a concrete language design.

Compiler-compiler generieren aus formalen Spezifikationen Komponenten für Compiler, um dort handgeschriebenen Code ersetzen. Solche Generatoren existieren für die lexikalische, syntaktische und semantische Anlayse, für Optimierer und die Coderzeugung. Es hat sich gezeigt, daß die Entwicklungszeit abnimmt und gleichzeitig das Vertrauen in die Korrektheit der Software steigt.

Die vorliegende Dissertation beschreibt einen Generator für Typchecker. Er erzeugt aus einer Spezifikation eines Typsystems, die in Form vom Typregeln gegeben ist, einen ablauffähigen Typchecker, der Typherleitungen mit Hilfe der gegebenen Regeln konstruiert. Abweichend von früheren Vorschlägen werden passende Definitionen für Typherleitung und Typregel durch Analyse existierender Typsysteme und der mathematischen Beweistheorie gewonnen. Auf diese Weise reflektiert der Ansatz die Struktur und Intention der Typsysteme, anstatt die Typregeln in einem bereits vorhandenen Formalismus auszudrücken.

Als Anwendungen werden Typchecker für imperative, objekt-orientierte und funktionale Sprachen, einschließlich der ML Typinferenz, formalisiert. Die Typregeln dieser Checker korrespondieren direkt mit den aus der Literatur bekannten. Da sie sich einzelnen Sprachkonstrukten zuordnen lassen, können sie in verschiedenen Checkern wiederverwendet werden.

Eine spezielle Anwendung ist die Sprache Saga für die Generische Programmierung. Die Generische Programmierung ist zu einem Standardansatz zur Erstellung verläßlicher und wiederverwendbarer Software geworden, insbesondere durch die weite Verbreitung der C++ Standard Template Library (STL). Der C++ Compiler kann allerdings die generischen Algorithmen erst dann prüfen, wenn konkrete Instanzen generiert werden. Fehler in den Algorithmen manifestieren sich daher erst bei der Benutzung. Saga löst dieses Problem durch eine neues Sprachdesign, das es erlaubt, generische Algorithmen der STL so zu überprüfen, daß die deklarierten Korrektheitsbedingungen erfüllt sind und die Instanzgenerierung nie fehlschlägt, wenn der Typchecker die Algorithmen akzeptiert. Damit realisiert Saga die Ziele des früheren Sprachvorschlags SuchThat in einem konkreten Sprachdesign.