Affiche-these-JN

    

SOUTENANCE de THESE

Jim NEWTON

Mardi 20 Novembre 2018 à 10h00

EPITA, 14-16 Rue Voltaire, 94270 Le Kremlin-Bicêtre

Salle KB 604

Representing and Computing with Types in Dynamically Typed Languages

Extending Dynamic Language Expressivity to Accommodate Rationally Typed Sequences

Abstract:

We present code generation techniques related to run-time type checking of heterogeneous sequences. Traditional regular expressions can be used to recognize well defined sets of character strings called rational languages or sometimes regular languages. Newton et.al. present an extension whereby a dynamic language may recognize a well defined set of heterogeneous sequences, such as lists and vectors.

As with the analogous string matching regular expression theory, matching these regular type expressions can also be achieved by using a finite state machine (deterministic finite automata, DFA). Constructing such a DFA can be time consuming. The approach we chose, uses meta-programming to intervene at compile-time, generating efficient functions specific to each DFA, and allowing the compiler to further optimize the functions if possible. The functions are made available for use at run-time. Without this use of meta-programming, the program might otherwise be forced to construct the DFA at run-time. The excessively high cost of such a construction would likely far outweigh the time needed to match a string against the expression.

Our technique involves hooking into the Common Lisp type system via the deftype macro. The first time the compiler encounters a relevant type specifier, the appropriate DFA is created, which may be a exponential complexity operation, from which specific low-level code is generated to match that specific expression. Thereafter, when the type specifier is encountered again, the same pre-generated function can be used. The code generated is of linear complexity at run-time.

A complication of this approach, which we explain in this report, is that to build the DFA we must calculate a disjoint type decomposition which is time consuming, and also leads to sub-optimal use of typecase in machine generated code. To handle this complication, we use our own macro optimized-typecase in our machine generated code. Uses of this macro are also implicitly expanded at compile time. Our macro expansion uses BDDs (Binary Decision Diagrams) to optimize the optimized-typecase into low level code, maintaining the typecase semantics but eliminating redundant type checks. In the report we also describe an extension of BDDs to accomodate subtyping in the Common Lisp type system as well as an in-depth analysis of worst-case sizes of BDDs.

Read the full text: Copy of thesis

Composition du Jury :

• GÉRAUD Thierry, Pr, Directeur de thèse, Professeur, EPITA, France
• VERNA Didier, Dr, Co-encadrant de thèse, EPITA, France
• STRANDH Robert, Pr, Rapporteur, Université Bordeaux, France
• COSTANZA Pascal, Dr, Rapporteur, Imec, Belgique
• RHODES Christophe, Dr, Goldsmiths, University of London, Department of Computing, Royaume Uni
• JOBSTMANN Barbara, Dr, École Polytechnique Fédérale de Lausanne (EPFL), Suisse
• BRESSON Jean, Dr, IRCAM / CNRS / Sorbonne Université, France