Towards Type Debugging using Partial Evaluation
In this study, we introduce a method of executing ill-typed programs. There are two advantages of executing an ill-typed program. The first advantage is that, after execution, the cause of the type error is easier to find because the distance between the cause of the type error and the part that conflicts with it is smaller. The second advantage is that even though the language is statically typed, ill-typed programs can be executed as much as possible.
The idea is to “freeze” the part of the program which is the most likely cause of type errors. Our approach to “transformational debugging” has three phases: In the first phase, we use the error messages of the compiler’s type inferencer to “freeze” (dynamize) parts of the program. In the second phase, the type inferencer is used to reduce the number of “frozen” parts. In the third phase, a partial evaluator evaluates the partially “frozen” program. During partial evaluation, the frozen parts are treated as dynamic and therefore remain as code without being evaluated, while the other parts are treated as static and evaluated.
This paper presents the generic algorithms for our debugging method, two heuristic strategies for the algorithms, and promising preliminary results. This work explores a novel avenue for partial evaluation: partial evaluation as a helpful tool for debugging.
Tue 17 JanDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30
|Fast Cryptographic Code via Partial Evaluation
Adam Chlipala Massachusetts Institute of Technology
|Towards Type Debugging using Partial Evaluation