Blame Prediction

: Early detection of type errors in dynamically typed programming languages

  • Dries Harnie ((PhD) Student)

Scriptie/masterproef: Doctoral Thesis


In the context of software development, programmers often use dynamically typed programming languages, which perform type tests at run-time and directly report any type errors. However, developing and debugging programs in such languages is difficult for a number of reasons. First, when a type error is reported, the programmer must identify the wrongly-typed value and trace back through the program to find out how and where it was computed. This place might be in a different part of a program and finding it requires a manual, time-consuming search. Second, there might be a large number of computational steps in between these two program locations, which slows down the edit-run-debug cycle by making the programmer wait.

In this dissertation we propose a program transformation called "blame prediction" for a small core language similar to the programming language Scheme. The driving idea is to make the type tests of built-in functions and operators explicit and perform them as early as possible without changing the program semantics. When such an early type test fails, the program "predicts blame" for primitive operations further down in the program. This solves both problems: first, the programmer can start tracing where and how the value is computed starting from the type test instead of the primitive operation, and second, some computational steps are bypassed, thereby reducing the wait.

The blame prediction transformation consists of three parts. The first part is built around a novel type system which not only infers types from dynamically typed programs, but also records any (run-time) type tests which must be made "along the way" in order for the program to succeed. Such types enable the propagation of type tests beyond function boundaries. Under this type system, recursive functions induce ever-growing recursive types, which we tackle using techniques from abstract interpretation. In addition, our type system makes a conservative estimation of which variables are mutated by expressions. Finally, every function application in the program is wrapped in a type test.

The second part moves these type tests upwards as far as possible, without changing the semantics of the input program. This means making sure no unbound variables are referenced and no type tests are performed which would otherwise not be performed. This part makes use of the mutation information from the first step: since type tests inspect the type of values inside variables, they may not be moved over expressions which mutate those variables.

The third part is a simplification step which eliminates redundant type tests. The result of this step — and of the blame prediction transformation — is a program similar to the input program, but augmented with special expressions which perform a type test and predict blame for labeled future expressions if they detect a type error.

We have applied the blame prediction transformation to two standard program corpora. We showed that it is capable of moving type tests upwards in a variety of programs, both statically (solving the first problem) and dynamically (solving the second problem). In addition, we found that the blame prediction transformation is able to eliminate a large fraction of the type tests in a dynamically typed program. Finally, we have proved that the blame prediction transformation does not introduce additional errors (either by referencing unbound variables or introducing extra type tests) and that it preserves the behaviour of its input program.
Datum Prijs11 sep 2015
Toekennende instantie
  • Vrije Universiteit Brussel
BegeleiderWolfgang De Meuter (Promotor), Christophe Scholliers (Co-promotor), Coen De Roover (Jury), Ann Nowe (Jury), Ann Dooms (Jury), Viviane Jonckers (Jury), Tom Schrijvers (Jury) & Jacques Noye (Jury)

Citeer dit