Type systems for safe strategic rewriting
Creators: name: Fu, Rongxiao
Publisher: name: The University of Edinburgh
Year: 2024
Subjects: optimisation
rewrite rules
strategy languages

description: Strategy languages enable programmers to compose rewrite rules into strategies and control their application. This is useful in programming languages, e.g., for describing program transformations compositionally, and also in automated theorem proving. Not all compositions of rewrites are correct, and it is not always easy for the programmers to spot erroneous strategy compositions in practice. Thus, we raise the question: how do we assist programmers to avoid mistakes and in writing correct composition of rewrites as strategies? As our proposed solution, type systems are a commonly used method to rule out erroneous programs and ensure that type-checked programs have expected properties, and in this thesis, we use type systems to capture the shape of rewritten terms and reject strategies which are guaranteed to fail at runtime for all possible inputs. There are previous works in designing type systems for strategies languages, but they either focus on the interactions of generic strategies instead of the correctness of each concrete individual composition, or lack important features such as customized strategy combinators. Initially inspired by the strategy language ELEVATE, this thesis presents three statically typed strategy languages assisting programmers to write correct strategies. The first language introduced in this thesis is Typed ELEVATE, which is equipped with a row-polymorphic type system working as the basis for the other two more advanced type systems. It uses structural row types to capture how rewriting transforms the shape of the rewritten programs, and it statically rejects strategies which lead to runtime pattern matching errors. We show a formalization of Typed ELEVATE together with its soundness proof, and the demonstration of its practical use for expressing compiler optimization strategies. However, there are still many practically useless strategies which can normally run without runtime errors, but always return failed rewriting results. To detect such unproductive strategies, we introduce the second language in this thesis, Rewrite St, a static type system combing the row-polymorphic types and a novel tracing system that keeps track of all possible legal strategy execution paths, while preserving as many of the useful features of Type ELEVATE as possible. Rewrite St introduces new concepts such as traces and unproductive strategies, but it still has many limitations such as weak formal guarantees, overly complex formalization and lack of recursive types. After discussing the issues of Rewrite St, we introduce the third language in this thesis, Core St, which also features a traced type system but addresses most of the issues. Core St simplifies the tracing mechanism, supports recursive types, and provides stronger formal guarantees. It raises warnings when parts of a composition are guaranteed to fail at runtime, and errors when no legal execution for a strategy is possible. We present a formalization of Core St, and formally proves its type soundness, shows that ill-traced strategies are guaranteed to fail at runtime and that well-traced strategy executions “can't go wrong”, meaning that they are guaranteed to have a possible successful execution path.