  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.
