Cookbook - Type System

Inference rules

This cookbook should give you quick answers and guidelines when designing types for your languages. For in-depth description of the typesystem please refer to the Typesystem section of the user guide.

Equality

Use type equation when the type of a node should always be a particular concrete type. Use the typeof command to declare that the type of the desired node should equal to a particular type.

rule typeof_StringLiteral {
      applicable for concept = StringLiteral as nodeToCheck
      applicable always
      overrides false

      do {
        typeof(nodeToCheck) :==: <string>;
      }
    }

Note quotation is used to refer to a type. <string> is equivalent to typing new node<StringType>(). The type of an element is equal to the type of some other element. For example, the to express that parentheses preserve the type of the wrapped element, the ParenthesizedExpression concept

declares:

rule typeOf_ParenthesizedExpression {
      applicable for concept = ParenthesizedExpression as parExpr
      applicable always
      overrides false

      do {
        typeof(parExpr) :==: typeof(parExpr.expression);
      }
    }

Inequality

When the types should be sub-types or super-types of other types, use the infer typeof command. See the ternary operator as an example:

rule typeOf_TernaryOperator {
  applicable for concept = TernaryOperatorExpression as toe
  applicable always
  overrides false

  do {
    infer typeof(toe.condition) :<=: <boolean>;
    infer typeof(toe) :>=: typeof(toe.ifTrue);
    infer typeof(toe) :>=: typeof(toe.ifFalse);
  }
}

The ForEachStatement concept illustrates how to solve quite an involved scenario. The type of the loop variable must be equal to the type of elements in the iterated collection, while the type of the collection must be a sub-type of either a sequence or an array of elements of the elementType type.

rule typeof_ForEachStatement {
  applicable for concept = ForEachStatement as forEachStatement
  applicable always
  overrides false

  do {
    node<ForEachVariable> variable = forEachStatement.variable;
    node<Expression> inputSequence = forEachStatement.inputSequence;
    if (inputSequence.isNotNull && variable.isNotNull) {
        var elementType;
        infer <join(sequence<%( elementType)%>| %( elementType)%[])> :>=: typeof(inputSequence);
        typeof(variable) :==: elementType;
    }
  }
}

Notice, we use var elementType to declare a variable, which we then use to tie together the type of the collection elements and the type of the loop variable. Also, %(...)% demarcates so called anti-quotation, which allows you to provide values from your local context into the AST you are manipulating or retrieve them back.

Replacement rules

Replacement rules indicate to the type system the possibility to replace one type with another. For example, NullType is a subtype of all types (except for primitive types) and so the type system can simply remove the inequation between NullType and BaseConcept.

replacement rule any_type_supertypeof_nulltype

applicable for  concept = NullType as nullType <: concept = BaseConcept as baseConcept

custom condition: ()->boolean {
  !(baseConcept.isInstanceOf(RuntimeTypeVariable));
}

rule {
  if (baseConcept.isInstanceOf(PrimitiveType) || baseConcept.isInstanceOf(PrimitiveTypeDescriptor)) {
    error "null type is not a subtype of primitive type" -> equationInfo.getNodeWithError();
  }
}

Replacement rules are also handy to declare covariance and contravariance. For example, covariance for sequences is declared in MPS as follows:

replacement rule sequence_subtypeOf_sequence

applicable for  concept = SequenceType as left <: concept = SequenceType as right

custom condition: true

rule {
  if (right.elementType.isNotNull) {
    infer left.elementType :<=: right.elementType;
  }
}

The original rule claiming that the left collection is a subtype of the right collection gets replaced with a rule ensuring that the type of elements in the left collection is a subtype of the type of elements in the right collection.

Subtyping rules

Subtyping rules allow you to specify where the particular type belongs in the type hierarchy. The rule returns a collection of types, which it identifies as its direct super-types. The following rule, for example, declares that Long variables can be cast to Float.

subtyping rule long_extends_float {
  weak = false
  applicable for concept = LongType as longType

  rule {
    return <float>;
  }
}

Here MPS declares, that LinkedList is a subtype of either a List, a Deque or a Stack:

subtyping rule supertypesOf_linkedlist {
  weak = false
  applicable for concept = LinkedListType as llt

  rule {
    nlist<> res = new nlist<>;
    res.add(<list<%( llt.elementType)%>>);
    res.add(<deque<%( llt.elementType)%>>);
    res.add(<stack<%( llt.elementType)%>>);
    return res;
  }
}

Comparison rules

When two types should be interchangeable, use comparison rules to define that. For example, the following rule makes NullType comparable with any type, except for primitive ones:

comparison rule  any_type_comparable_with_nulltype

applicable for  concept = BaseConcept as baseConcept , concept = NullType as nullType

rule {
   if (baseConcept.isInstanceOf(PrimitiveType) || baseConcept.isInstanceOf(PrimitiveTypeDescriptor)) { return false; }
   return true;
}
weak = false

Similarly, the MapType from BaseLanguage and the Map interface from Java (here refered to through the ClassifierType concept inside a pattern) should be comparable:

comparison rule  map_type_comparableWith_Map

applicable for  concept = MapType as mapType , > Map<# KEY, # VALUE> < as classifierMapType

rule {
   return true;
}
weak = true

Substitute Type rules

These instruct the type-system to replace nodes representing a type with defined substitutes.

For example, one might decide to use different types for different program configurations, such as using int or long depending on whether the task requires using one type or another. This is different from simply using the generator to produce the correct "implementation" type, as the substitution is done at the time the typechecking is performed, so possible errors can be caught early.

In its simplest form the type substitution can be used by creating an instance of Substitute Type Rule in the typesystem model.

substitute type rule substituteType_MyType {                                                                                       
  applicable for concept = MyType as mt                                                                          
                                                                                                                                                 
  substitute {                                       
    if (mt.isConditionSatisfied()) { 
      return new node<IntegerType>;
    } 
    null; 
  }                                

}                                                                                                                                                                                                   

The Substitute Type Rule is applicable to nodes that represent types. Whenever a new type is introduced by the typechecker, it searches for applicable substitution rules and executes them. The rule must either return an instance of `node<>` as the substitution, or null value, in which case the original node is used to represent the type (the default behaviour).

One other possibility to overrides types used by the typechecker comes with the use of node attributes. If there is a node attribute contained by the original type node, the typechecker tries to find a Substitute Type Rule applicable to the attribute first. This way one can override the type nodes even for languages, which implementation is sealed.

substitute type rule substituteType_SubstituteAnnotation {                                                                                       
  applicable for concept = SubstituteAnnotation as substituteAnnotation                                                                          

  substitute {                                                                                                                                        
    if (substituteAnnotation.condition.isSatisfied(attributedNode)) { 
      return substituteAnnotation.substitute; 
    } 
    null; 
  }
}                                                                                                                                                

The rule above is defined for the attribute node, and it's the attribute node that is passed to the rule as the explicit parameter. The rule can check whether the condition for substituting the type node is satisfied, and it can also access the attributed node representing original type via attributedNode expression.

Checking and Quick-fixes

Checking rules become part of the MPS code analysis process and will report found issues to the user interactively in the editor. For example, this is a check for superfluous type casts:

checking rule CheckExcessTypeCasts {
  applicable for concept = CastExpression as expr
  overrides none

  do {
    if (isStrongSubtype(expr.expression.type :<< expr.type)) {
      info "Typecast expression is superflous" -> expr ;
    }
  }
}

Now you can define a quick-fix that will pop-up to the user whenever the problem above is reported. The user can then quickly invoke the quick-fix to correct the reported issue.

quick fix RemoveExcessTypeCast

arguments:
node<CastExpression> castExpr

fields:
<< ... >>

description(node)->string {
  "Remove Excess Typecast";
}

execute(node)->void {
  castExpr.replace with(castExpr.expression);
}

The hook the quick-fix to the reported error, you need to specify the quick-fix as intention linked with info message(optional):

Additionally, you can pass parameters to the quick-fix and mark it with apply immediately, in which case the quick-fix will be applied automatically as soon as the error is discovered in the editor.

When-concrete, overloaded operations

When-concrete blocks allow you to perform type checks once the type a node has been calculated. In the example below we are checking, that the calculated type of an operation matches the type suggested by the operation type command based on the operator overriding rules:

rule typeof_BinaryOperation {
  applicable for concept = BinaryOperation as operation
  overrides false

  do {
    when concrete (typeof(operation.leftExpression) as leftType) {
      when concrete (typeof(operation.rightExpression) as rightType) {
        node<> opType = operation type( operation , leftType , rightType );
        if (opType.isNotNull) {
          typeof(operation) :==: opType;
        } else {
          error "operation is not applicable to these operands" -> operation;
        }
      }
    }
  }
}

Last modified: 18 June 2020