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, but also in automated theorem proving, where related ideas have been studies with tactics languages. Clearly, not all compositions of rewrites are correct, but how can we assist programmers in writing correct strategies? In this paper, we present a static type system for strategy languages. We combine a structural type system capturing how rewrite strategies transform the shape of the rewritten syntax with a novel tracing system that keeps track of all possible legal strategy execution paths. Our type system 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 our strategy language and novel tracing type system, and formally prove its type soundness. We present formal results, showing 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.

翻译：策略语言使程序员能够将重写规则组合成策略并控制其应用。这在编程语言中非常有用，例如用于组合式地描述程序转换，同时在自动定理证明中也有应用，其中相关思想已通过策略语言得到研究。显然，并非所有重写组合都是正确的，但如何帮助程序员编写正确的策略？在本文中，我们提出了一种针对策略语言的静态类型系统。我们将一个结构类型系统（用于捕获重写策略如何转换重写语法的形状）与一个新颖的跟踪系统（用于跟踪所有可能的合法策略执行路径）相结合。当组合的某些部分在运行时保证失败时，我们的类型系统会发出警告；当策略没有合法执行路径时，则会报告错误。我们提出了策略语言和新颖的跟踪类型系统的形式化定义，并正式证明了其类型安全性。我们展示了形式化结果，表明标记错误的策略在运行时保证会失败，而标记正确的策略执行“不会出错”，即保证存在一条可能的成功执行路径。