Row-Polymorphic Types for Strategic Rewriting

TL;DR

This paper introduces a row-polymorphic type system for strategy languages that helps ensure correctness of program transformations and reasoning about their effects, aiding compiler optimization and verification.

Contribution

It presents a novel type system that statically enforces meaningful rewrite compositions and enables reasoning about program shape transformations.

Findings

Type system prevents invalid rewrite compositions.

Supports formal reasoning about program transformations.

Demonstrated practical use in compiler optimization strategies.

Abstract

We present a type system for strategy languages that express program transformations as compositions of rewrite rules. Our row-polymorphic type system assists compiler engineers to write correct strategies by statically rejecting non meaningful compositions of rewrites that otherwise would fail during rewriting at runtime. Furthermore, our type system enables reasoning about how rewriting transforms the shape of the computational program. We present a formalization of our language at its type system and demonstrate its practical use for expressing compiler optimization strategies. Our type system builds the foundation for many interesting future applications, including verifying the correctness of program transformations and synthesizing program transformations from specifications encoded as types.