Terms provide a generic, untyped format to represent tree-structured data. Stratego transformations can transform such data, but require at least that the arities of term constructors that are used in rules are declared.
Starting with Stratego 2, the types of terms and term transformations may be declared and checked in more detail1.
A signature declares the shape of well-formed terms using sort declarations, constructor declarations, and overlays.
A sort is determined by an identifier and optionally has arguments.
A sort (or type) identifies a collection of well-formed terms.
Convention: Sort identifiers start with a capital letter.
A constructor declaration has the form
$Constructor : $Sort * ... * $Sort -> Decl
and declares a constructor name, the sorts of the argument terms, and the sort of the constructed term.
Convention: Constructor identifiers start with a capital letter.
Example: The constructor declaration
Assign : ID * Exp -> Stmt
defines the constructor
Assign with input sorts
Exp and output sort
e are terms of sort
Exp, respectively, then
Assign(x, e) is a term of sort
When the list of argument sorts is empty the arrow can be omitted:
$Constructor : Decl
Example: The constructor declaration
True : Bool
True() is a term of sort
Note that the parentheses are required.
True is a variable.
The Stratego1 compiler only checks the arity of constructor applications against the signature. The Stratego2 compiler uses signature definitions to type check code if it has been given a type signature.
An injection is a constructor without name and with a single argument.
: $Sort -> $Sort
Injections include an entire type as a subtype of another type without cluttering the tree structure.
The type constructor
List(_) is for typing homogenous lists.
Exmample. The type
List(Exp) represents lists of expressions
Stratego2 supports user-defined polymorphic types. That is, sorts can have parameters.
For example, the following signature defines the type of priority queues, polymorphic in the carrier type, in which the priority is determined by the length of the list.
signature sorts PrioQ(*) constructors NilQ : PrioQ(a) ConsQ : a * int * List(a) * PrioQ(a) -> PrioQ(a)
($TermType * ... * $TermType)
Tuple terms can be typed in strategy types. Currently, tuple types cannot be used in term signatures.
An overlay defines a term abbreviation. An overlay definition has the form
$Constructor($ID, ..., $ID) = $Term
and defines that applications of the constructor should be expanded to the term.
$Id($StrategyType, ... | $TermType, ...) :: $TermType -> $TermType
A transformation type defines the signature of a transformation with name
$Id with the types of its strategy arguments and term arguments, the type of the 'current term' to which the transformation is applied, and the type of the term that is returned, if the transformation succeeds.
Transformation types are declared in
$Id($StrategyType, ...) :: $TermType -> $TermType
When a transformation only has strategy parameters, the bar can be left out.
$Id :: $TermType -> $TermType
When a transformation also has no strategy parameters, the parentheses can be left out as well.
$TermType -> $TermType
The type of a transformation/strategy argument is an arrow from a term type to a term type.
Note that transformation strategies cannot be reified as terms.
Type dynamic, written
?, represents the unknown type.
Stratego2 is a gradually typed language in order to facilitate the migration from (mostly) untyped Stratego1 code to typed Stratego2 code. Furthermore, some patterns in Stratego cannot be typed statically.
When used as a strategy type
? -> ?.
///syntax of casts
Gradual type systems allow a term with the dynamic type to be used in any place where a static type is required. Stratego2 will insert a type cast at such a point to check at run time that the term is type-correct. This way, a Stratego program halts execution in predictable places when a run time type error occurs. There can be no run time type errors in fully statically typed code either, only at the boundary between dynamically and statically typed code.
A type preserving transformation transforms any type to itself (or fails).
In signatures, a type preserving transformation is indicated with
Example. The type declaration
topdown(s : TP) :: TP
declares that the
topdown strategy is type preserving if its argument strategy is.
The type-checking for a type preserving transformation is very strict. It should be in terms of other type preserving transformations, or match the input term to a specific type and return a term from that specific type.
Given the definition of a term sort
is(S) strategy checks whether a term is of sort
S and fails if that is not the case.
Example. The strategy
<is(Exp)>t checks that term
t conforms to the signature of sort
is(S) strategy uses the same mechanism as type casts for checking a term type at run time.
Jeff Smits and Eelco Visser. Gradually typing strategies. In Ralf Lämmel, Laurence Tratt, and Juan de Lara, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, Virtual Event, USA, November 16-17, 2020, 1–15. ACM, 2020. URL: https://doi.org/10.1145/3426425.3426928, doi:10.1145/3426425.3426928. ↩
Created: September 15, 2023