Type System

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

-- EelcoVisser - 1999

By now there are several proposals for typing languages with generic traversal strategies. RalfLaemmel proposes a typed version of SystemS. It would be interesting to implement his system in the StrategoCompiler and see where it breaks. -- EelcoVisser - 22 Nov 2001

---

ToDo | Contributions by EelcoVisser