Type System
Stratego -- Strategies for Program Transformation
Currently Stratego is very weakly typed. The reason for the weak type system is that it is not clear how to combine strong typing with generic traversals and transformations.
Here is a relevant quote (I don't remember where I got it from):
Stefan Kahrs in [Kah96] discusses the notion of completeness--programs which never go wrong can be type-checked--which complements Milner's notion of soundness--type-checked programs never go wrong [Mil78].
It is not difficult to make a sound type system for Stratego based on standard type systems, but that would restrict the range of useful Stratego programs too much. What is needed is a complete
type system in the sense of the citation that supports the full range of Stratego programming.
Here are some properties that a type system might check
- Given a term of this type, this strategy returns a term of that type
- This strategy always succeeds
- Given an initial term of this type or form, this strategy will succeed and transform it to a term in this format
ToDo | Contributions by
EelcoVisser