Technische Universität Darmstadt Universitäts- und Landesbibliothek

Die Dokumente in PDF 1.3 (mit Adobe Acrobat Reader 4.0 zu lesen):

Abstract auf Deutsch:

Typsysteme auf Basis des von R. Milner entwickelten Konzepts des parametrischen Polymorhpismus zeichnen sich dadurch aus, daß jedes wohltypisierte Programm eine eindeutige denotationale Semantik besitzt, die Typfehler zur Laufzeit verhindert. Darüber hinaus kann jedem typisierbaren Programm ein allgemeinster Typ zugeordnet werden, der alle möglichen Instanztypen durch einen einzigen Typausdruck über unsortierten Typvariablen darstellt, und dieser Typausdruck kann auf Basis eines Unifikationsalgorithmus für Typausdrücke berechnet werden. Dabei sind Typangaben für vom Programmierer eingeführte Bezeichner optional.

Überladene Operatoren bzw. Konstanten werden in traditionellen und auch in moderneren objekt-orientierten Sprachen als rein syntaktische Erleichterungen behandelt: ein Operator darf eine endliche Menge verschiedener Typen annehmen und zur Übersetzungszeit muß für sämtliche Vorkommen eines überladenen Operators bestimmt werden, welche Überladungsinstanz vom Programmierer an der entsprechenden Programmstelle intendiert war. Diesen Prozeß bezeichnet man üblicherweise als Überladungsauflösung.

Fügt man einem parametrisch polymorphen Typsystem Überladungen auf der Grundlage dieses Ansatzes hinzu, dann erhält man einen NP-vollständigen Typinferenzalgorithmus. Darüber hinaus kann ein solches Typsystem zwar die Verwendung überladener Operatoren ermöglichen, aber es erlaubt nicht deren Abstraktion in der Definition neuer Funktionen, da ein Ausdruck mehr als einen Typ besitzen kann.

In der vorliegenden Arbeit wird das Konzept der parametrischen Überladungen vorgestellt, das diese Nachteile vermeidet und dabei sämtliche Vorteile des parametrischen Polymorphismus beibehält: jeder typisierbare Ausdruck besitzt einen allgemeinsten Typ, typisierbare Programme führen nie zu Laufzeitfehlern, die Komplexität des Inferenzalgorithmus ist polynomial zeitbeschränkt und überladene Operatoren können in Funktionsdefinitionen abstrahiert werden.

Darauf aufbauend untersuchen wir Typinferenzsysteme für Sprachen, die zusätzlich zu Überladungen auch noch implizite Konversionen unterstützen. Dazu definieren wir ein generisches Typinferenzsystem für eingeschränkte Typen und zeigen, daß auch in einem solchen System allgemeinste Typen existieren und Typisierbarkeit für bestimmte Restriktionsklassen entscheidbar bleibt. Abschließend zeigen wir, daß parametrische Überladungen mit regulären Typen kombiniert werden können.

Abstract auf Englisch:

Type systems based on R. Milner's concept of parametric polymorphism are recognized by the following facts: every well typed program has a uniquely defined denotational semantics, which ensures that the evaluation of a program will never produce a runtime type error. Additionally, every well typed program has a principal type such that every other type is an instance of the principal type. The principal type is a type expression over unsorted variables and can be computed by a type inference algorithm based on Robinson's unification algorithm.

In traditional programming languages, overloaded operators and constants are treated as pure syntactic sugar: an overloaded operator can have a finite number of unrelated types and the type analysis component must determine for each occurrence of an overloaded operator, which of its overloaded instances was intended by the programmer. This process is usually called overloading resolution.

Adding overloaded operators based on this concept to a parametrically polymorphic language has two drawbacks: since each programmer declared identifier is reqired to have a simple type, the type inference algorithm becomes NP-complete and overloaded operators cannot be abstracted over in user defined functions.

In this thesis we define the concept of parametric overloading, which avoids these problems and keeps all nice properties of parametric polymorphism: principality of types, absence of runtime errors for well typed programs, polynomially time bounded type inference algorithm and full abstraction over overloaded operators.

Building on these results, we investigate a type system for a language which additionally supports implicit coercions. We define a generic inference system based on the concept of constrained types, show that principal types exist for this system and typability remains decidable for a special class of constraints. Finally we show that parametric overloading can be combined with regular types.