TU Darmstadt / ULB / TUprints

Co-Contextual Type Systems: Contextless Deductive Reasoning for Correct Incremental Type Checking

Kuci, Edlira (2020)
Co-Contextual Type Systems: Contextless Deductive Reasoning for Correct Incremental Type Checking.
Technische Universität Darmstadt
doi: 10.25534/tuprints-00011419
Ph.D. Thesis, Primary publication

[img]
Preview
Text
EdliraKuciDissertation.pdf
Copyright Information: CC BY-SA 4.0 International - Creative Commons, Attribution ShareAlike.

Download (1MB) | Preview
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Co-Contextual Type Systems: Contextless Deductive Reasoning for Correct Incremental Type Checking
Language: English
Referees: Mezini, Prof. Dr. Mira ; Ostermann, Prof. Dr. Klaus ; Erdweg, Prof. Dr. Sebastian
Date: February 2020
Place of Publication: Darmstadt
Date of oral examination: 25 March 2019
DOI: 10.25534/tuprints-00011419
Abstract:

This thesis proposes a novel way of performing type checking, whose results are incremental, depending on the provided local information. This new way of type checking is called co-contextual, where all context information of expressions, methods, classes, etc., is removed. Instead, we introduce corresponding structures using requirements. Standard type systems are translated to the co-contextual ones systematically using dualism as technique. Type systems play an important role to prevent execution errors from occurring during runtime. They are used to check programs statically for potential errors. Programs are type checked against a given set of rules. Depending on these rules programs are well-typed or not. The set of these rules is called typing rules. Each type rule associates types to the constructs of a program given a certain context. There can be different forms of contexts, depending on the features of the typed programming language. Functional languages use a typing context of variables and their types; object-oriented (OO) languages use additional class tables. Class tables are used for example to ensure that method and class declarations are well-typed. Type checking is performed top-down. While traversing the syntax tree of a program, typing contexts are extended with information on the expressions and their types. In case of OO, class tables are extended with clauses from class declarations, including the class members, i.e., fields, methods, or constructors. Contexts are passed through the nodes of the syntax tree in order to coordinate type checking between them. Therefore, while traversing the syntax tree top-down, the type checker creates dependencies between otherwise independent subexpressions. This way, it inhibits incrementalization and parallelization of type checking. That is, a change to a node of the syntax tree would require to redo the type check of the whole syntax tree. In this thesis a novel formulation of type systems is proposed, in order to remove dependencies between subexpressions. We propose a co-contextual formulation of typing rules that depends only on the local program constructs, e.g., expressions, methods, classes. The co-contextual typing rules have as conclusion a type and sets of requirements. That is, contexts and class tables are replaced by the dual concept of context and class table requirements. In addition, operations on contexts and class tables are replaced by new dual operations on requirements. The co-contextual type checker traverses a syntax tree bottom-up and merges context requirements of independently checked subexpressions. We describe a method for systematically constructing a co-contextual formulation of type rules from a regular context-based formulation and we show how co-contextual type rules give rise to incremental type checking. We derive co-contextual type checkers for functional and OO languages. As a representative of functional languages we consider PCF and extensions of it: records, parametric polymorphism, structural subtyping and let-polymorphism. Also, we investigate featherweight java (FJ) as the basis of OO languages and extensions of it: method overloading and generics. We build a1 co-contextual type checker for FJ enabling key features of OO languages: subtype polymorphism, nominal typing and implementation inheritance. The dualism between the co-contextual and contextual type systems preserves the correctness of the contextual calculus. That is, we prove the correctness of the co-contextual calculus via the equivalence between contextual type rules and their co-contextual formulations. We implemented an incremental type checker for PCF along with a performance evaluation showing that co-contextual type checking has performance comparable to standard context-based type checking, and incrementalization can improve performance significantly. Regarding FJ, we implemented a co-contextual type checker with incrementalization and compared its performance against javac on a number of realistic programs. Our performance evaluation shows significant speedups for the co-contextual type checker with incrementalization in comparison to javac.

Alternative Abstract:
Alternative AbstractLanguage

Diese Arbeit schlägt einen neue Ansatz für Typsysteme vor, in dem die Ergebnisse einer Überprüfung sich inkrementell warten lassen. Die inkrementelle Wartung steht hierbei in Abhängigkeit zu der bereitgestellten lokalen Information. Diese neue Art der Typenüberprüfung wird als ko-kontextuell bezeichnet, wobei alle Kontextinformationen von Ausdrücken, Methoden, Klassen usw. entfernt werden. Stattdessen werden Strukturen eingeführt, welche die entsprechenden Informationen als Bedingungen darstellen. Standard Typsysteme werden systematisch mit Hilfe einer Dualismustechnik in die ko-kontextuellen Systeme übersetzt. Typsysteme spielen eine wichtige Rolle bei der Prävention von Laufzeitfehlern. Sie wer- den genutzt um Programme statisch auf potentielle Fehler zu prüfen. Die Typüberprüfung von Programmen wird auf der Basis vorgegebener Regeln des Typsystems durchgeführt. Diese Regeln werden im allgemeinen als Typregeln bezeichnet. Typregeln assoziieren Typen mit den Konstrukten eines gegebenen Programmes und eines dem Programm gemäßen Kontextes. Es gibt verschiedene Arten von Kontexten, die sich aus den Merk- malen der typisierten Programmiersprache ableiten. Funktonale Programmiersprachen nutzen einen Typkontext bestehend aus Variablen und deren Typ; objektorientierte (OO) Sprachen nutzen zusätzliche Klassentabellen als Kontext. Klassentabellen werden zum Beispiel eingesetzt um zu überprüfen das Klassen- und Methodendeklarationen wohltypisiert sind. Die Typenprüfung erfolgt beim Durchlaufen des Syntaxbaums eines Programms von oben nach unten. Hierbei werden die Kontexte um Informationen über die Ausdrücke und deren Typen erweitert. Im Falle von OO werden Klassentabellen um Klauseln aus Klassendeklarationen erweitert, einschließlich deren Klassenmitglieder, d.h. Felder, Meth- oden oder Konstruktoren. Kontexte werden durch die Knoten des Syntaxbaums gereicht, um die Typüberprüfung zwischen ihnen zu koordinieren. Daher erzeugt die Typüberprü- fung beim Durchlaufen des Syntaxbaums von oben nach unten Abhängigkeiten zwischen ansonsten unabhängigen Teilausdrücken. Diese Art der Typüberprüfung verhindert die Inkrementalisierung und Parallelisierung der Prüfung. Das heißt, eine Änderung an einem Knoten des Syntaxbaums würde erfordern, die Typprüfung des gesamten Syntaxbaums erneut durchzuführen. Diese Arbeit schlägt eine neue Formulierung bestehender Typsysteme vor, um Ab- hängigkeiten zwischen Teilausdrücken zu entfernen. Wir stellen eine ko-kontextuelle Formulierung von Typregeln vor, die sich nur auf lokale Programmkonstrukte bezieht, zum Beispiel auf Ausdrücke, Methoden oder Klassen. Die ko-kontextuellen Typregeln haben als Schlussfolgerung einen Typ und Mengen von Bedingungen. Das heißt, Typkontext und Klassentabellen werden durch das duale Konzept von Kontext- und Klassentabel- lenbedingungen ersetzt. Außerdem, werden Operationen, die auf dem Typkontext 7 und den Klassentabellen definiert sind, durch entsprechende duale Operationen ersetzt. Die ko-kontextuelle Typüberprüfung durchläuft den Syntaxbaum von unten nach oben und führt die Kontextbedingungen von unabhängigen Teilausrücken zusammen. Wir Beschreiben eine systematische Methode für die Konstruktion von ko-kontextuellen Typregeln ausgehend von einer kontextbasierten Formulierung der Typregeln und zeigen wie ko-kontextuelle Typregeln die Inkrementalisierung der Typüberprüfung nutzbar machen. Wir überführen kontextbasierte Typüberprüfung in eine ko-kontextuelle Formulierung für Funktionale- und OO-Sprachen. Als Vertreter funktionaler Sprachen betrachten wir PCF und seine Erweiterungen: Records, parametrischer Polymorphismus, strukturelle Subtypisierung und Let-Polymorphismus. Außerdem untersuchen wir Featherweight-Java (FJ) als Grundlage für OO-Sprachen und deren Erweiterungen: Methodenüberladung und Generics. Wir entwickeln eine ko-kontextuellen Typüberprüfung für FJ, welche die wichtigsten Merkmale von OO-Sprachen ermöglicht: Subtyp-Polymorphismus, nom- inale Typisierung und Vererbung von Implementierungen. Der Dualismus zwischen dem ko-kontextuellen und dem kontextbasierten System erhält die Korrektheit der kon- textbasierten Formulierung. Das heißt, wir beweisen die Korrektheit der ko-kontextuellen Formulierung durch die Äquivalenz zwischen kontextbasierten Typregeln und ihren ko- kontextuellen Entsprechungen. Wir haben eine ko-kontextuelle inkrementelle Typüberprüfung für PCF implemen- tiert und stellen diese zusammen mit einer Leistungsbewertung vor, die zeigt, dass die gesamte ko-kontextuelle Typprüfung eine vergleichbare Leistung mit die standardmäßige kontextbasierte Typprüfung aufweist und die Inkrementalisierung die Leistung deutlich verbessern kann. Bezüglich FJ, haben wir eine ko-kontextuelle inkrementelle Typüber- prüfung implementiert und deren Leistung mit javac in einer Reihe von realistischen Programmen verglichen. Unsere Leistungsbewertung zeigt eine signifikante Verbesserung der Geschwindigkeit für ko-kontextuelle inkrementelle Typüberprüfung im Vergleich zu javac.

German
URN: urn:nbn:de:tuda-tuprints-114194
Classification DDC: 000 Generalities, computers, information > 004 Computer science
Divisions: 20 Department of Computer Science > Software Technology
Date Deposited: 18 Feb 2020 07:25
Last Modified: 18 Feb 2020 07:25
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/11419
PPN: 460773356
Export:
Actions (login required)
View Item View Item