Gradual Types for Stratego - Demo Edition

Jeff Smits

Stratego is a term transformation language that inspired many a functional programming library for “generic programming”: generic traversal over data. Most of these libraries have the downside that they are all more limited in expressive power, because they work on typed tree representations. In Stratego, we can write arbitrary rewrite strategies that define the traversal over data, because Stratego is more dynamically typed. The upside of having typed trees though, is that you can quickly catch typing mistakes. Bugs in Stratego code can be a pain to debug, especially in situations with backtracking.

It’s the traditional trade-off, but we want better for Stratego. A way that we don’t give up expressive power, a way that we can keep using the code of today, and have a gradual migration path to a more typed world, with more up-front guarantees. And that can be realised through a gradual type system. After many years of thinking about how to capture the full power of Stratego generic traversal in a static type system, the simple solution turns out to be: don’t. Instead we keep code around generic traversal dynamically typed, but add a simple type system that works for most rewrite rules.

In this talk/demo I’ll go into the thoughts and decisions we have made so far for the type system and the planned implementation. I’ll show examples with the prototype type checker, a bidirectional type checker written in Stratego that can show warnings and errors in various situations already. There will be time for questions and writing little code snippets to see what the type checker does.

---

Previous: Hendrik van Antwerpen | Incremental Type Checkers using Scope Graphs
Next: Arjen Rouvoet | Demo of Intrinsically Typed Compilation of Imperative Code in Agda