How to make operator overloading with type inference using MPS type system?

  • 2
  • 22

I am creating an F#-like language with type inference.
Now, I want to have overloaded operators which participate on the type inference process.
Say, I have a code like this
fun xy (i) =  
    let sum = i + 1
    sum            

I want the i and sum to have inferred type of int and the xy will have the inferred type int->int.

In other case
fun xyz (i:int[]) =  
    let sum = i + 1
    sum            

I want the sum to be of type int[] and the xyz to be of type int[]->int[].
In this case, the (+) would use an array plus scalar addition semantics which will return another array.

MPS has built-in support for operator overloading via the overloaded operations rules and the operator type(...) operation.
But, to infer the operator type the operands must be already concrete, so, it cannot be used in situation like I've described above for the xy function where the i would not ever become concrete (while for the xyz case it would work just fine as the type of i will become concrete).

So, I want to use the built-in support for operator overloading (or similar extensible mechanism) while I want to have the ability to specify the default inferred type of the opposite operand when there is known the operator and the type of only one side of the operator (eventually also the default inferred types of both operands when only the operator is known).

If there is an "else" clause of the "when concrete" clause, the problem is easy to solve.
Is there something like that? Or, why the "when conrete" does not have an "else" branch?

I've tried to use join(..) type to restrict the opposite operand to only possible types (typeof(operand) :<=: join(possible-types)), but the final type will stay the join(...) type at the end.

My last (hacky) solution is to use an extra parameterized type (BinaryOperandType) which holds the possible default inferred type. Then, there is a replacement rule which says that if the subtype of this BinaryOperandType type isInstanceOf(RuntimTypeVariable), then the variable should infer the opposite type:
replacement rule replace_inferWhenNotConcrete_binaryOperandType                                                                                                                            
                                                                                                                                                                                           
applicable for  concept = BaseConcept as any <: concept = BinaryOperandType as binaryOperandType                                                                                           
                                                                                                                                                                                           
custom condition: true                                                                                                                                                                     
                                                                                                                                                                                           
rule {                                                                                                                                                                                     
  if (any.isInstanceOf(RuntimeTypeVariable)) { 
    infer any :<=: binaryOperandType.oppositeType; 
  } else { 
    // do nothing, the any has its type, so no need to infer from the opposite 
  }
}     


The rule is not invoked as is, however. The type system infers the operand type as the BinaryOperandType instance itself and does not use the above replacement rule (it solves the inequation from the typeof_BinaryExpr rule (see below) by making the variable to become the BinaryOperandType instance itself).
Is this a bug or an intended feature of the type system engine? (I mean, if the type system engine should prefer inferring a type variable's final type from its "lower bound type" even when there are some other replacement rules at hand ?)

To workaround it, I've added to the BinaryOperandType an extra child which holds an aliased type variable which causes the BinaryOperandType instances to be non-concrete and somehow makes the engine to use the above rule.

For completeness, here is a prototype of the typeof_BinaryExpr inference rule, which only tries to infer the opposite operand type when symmetric. That is, the default inferred type of the opposite operand will be the concrete one if the operator will support the symmetric operation:

rule typeof_BinaryExpr {                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          
  applicable for concept = BinaryExpr as binaryExpr                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               
  overrides false                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  
  do {                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            
    when concrete (typeof(binaryExpr.leftExpr) as leftType) { 
        node<> inferredFromLeft = operation type(binaryExpr, leftType, leftType); 
        if (inferredFromLeft.isNotNull) { 
           var rt; 
           typeof(binaryExpr.rightExpr) :==: rt; 
           infer typeof(binaryExpr.rightExpr) :<=: <binop ^(  binaryExpr )^ oposite %( leftType)% is left false my var %( rt)%>; 
           // typeof(binaryExpr.rightExpr) :==: <join(%( leftType)%)>; 
        } 
        when concrete (typeof(binaryExpr.rightExpr) as rightType) { 
          node<> opLeftType = leftType; 
          node<> opRightType = rightType; 
          node<> resultType = operation type(binaryExpr, opLeftType, opRightType); 
          if (resultType.isNotNull) { 
             typeof(binaryExpr) :==: resultType; 
          } 
        } 
    } 
   
    when concrete (typeof(binaryExpr.rightExpr) as rightType) { 
      node<> inferredFromRight = operation type(binaryExpr, rightType, rightType); 
      if (inferredFromRight.isNotNull) { 
        var lt; 
        typeof(binaryExpr.leftExpr) :==: lt; 
        infer typeof(binaryExpr.leftExpr) :<=: <binop ^(  binaryExpr )^ oposite %( rightType)% is left true my var %( lt)%>; 
        // typeof(binaryExpr.leftExpr) :==: <join(%( rightType)%)>; 
      } 
    }
  }                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               
}                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 



This seems to work well in some cases without problems, but in others there is an error: "Error: Recursive types not allowed"
The types are inferred as expected, but the error is there ...

Do you know how to solve these problems?
Or generally, how to implement operator overloading with type inference in the right way using the MPS type system aspect?


(PS: it seems there is a bug in type system aspect in MPS 3.0.3 IDE integration: when I change anything in the type system aspect and rebuild my language, the old rules are still used in my sandbox solution's programs ... I've to restart MPS every time ...)






Question is not answered.
Unfortunately, errors are not shown/working in the Typesystem Trace (ctrl+X) (a reported issue: MPS-17916).
I was brave enough to investigate more deeply by stepping the type system engine, thanks MPS being open source, in IDEA :)
Must say, type system is gorgeous! (and MPS in general is gorgeous; the only thing I would wish, it'd been coded in a "more appropriate language for the domain" than plain Java ... base language is much better, but IMHO still not enough).

The "Error: Recursive types not allowed" is a situation when there is an equation where one side is a type variable and the other side is some shallowly concrete type which has the same type variable inside it (more precisely, the same is with respect to groups of aliased variables (by :==:) where each group has representatives which are actually tested for being the same; also, when both sides of the equation are vars, it is ok, it is an alias).
So, the error is what it says, the type engine does not cope with recursive equations.
In my case the erroneous equation has the type var of the unsolved operand on one side and the other side is <binop ...>, like this

a :==: <binop + opposite int is left true my var a>

which is a recursive equation (because of the a inside the right side) and comes from the solution of
var lt; 
typeof(binaryExpr.leftExpr) :==: lt; 
infer typeof(binaryExpr.leftExpr) :<=: <binop ^(  binaryExpr )^ oposite %( rightType)% is left true my var %( lt)%>; 

when there were no other inequalities that would affect the a type-var, so it was made :==:.
Because there was the error, the inequality was not solved, so my replacement rule could be effectively used instead as I expected.

This way is of course a non-solution to my problem...
Still looking for another solution,
have you some clue?

At last, after several iterations between MPS and IDEA stepping the type system engine, I've come up with a solution.

The type system treats recursive inequalities of the form
< ... var ... > :<=: var
in a special way (IMHO there should be also treatment of the opposite form see MPS-19358).
It tries to solve it AFTER solving all equalities plus non-recursive inequalities.
So, when everything else does not make a recursive inequality concrete, it will attempt to solve it by application of a replacement rule, if there is a matching one; eventually it also tries to check subtype relation in a normal way (calculating it via isSubType()).

This is almost what I need to implement the operator overloading with possibility to infer operand types when they are not to be concrete from another context.
I've created a special internal type:
concept BinaryOperationType extends Type
  children:
  leftType : IType[1]
  rightType : IType[1]
  recursiveVar : IType[1]

  references:
  binOperation : BinaryExpr[1]
which will hold all needed information to be used in a replacement rule to infer result type and eventually the operand types when not concrete yet.
Rule for my binary expression is now:
rule typeof_BinaryExpr {
 applicable for concept = BinaryExpr as binaryExpr                                                                                 
  overrides false
  do {
    var recVar; 
    infer <binop type( %( typeof(binaryExpr.leftExpr))% ^(  binaryExpr )^ %( typeof(binaryExpr.rightExpr))% var %( recVar)% )> :<=: recVar; 
    when concrete (recVar as conreteType) { 
      infer conreteType :<=: typeof(binaryExpr); 
    } 
  }
}
The recVar is there to force the type system to wait as long as possible to infer all possible concrete types of the operands.
Then the recVar is assigned a final result type by the following replacement rule which will cause the above when concrete to be invoked and to infer a concrete type for the binaryExpr. The following rule is rather long, sorry, not enough time to make a it short...
replacement rule replace_binary_operation_type
applicable for  concept = BinaryOperationType as binop <: concept = BaseConcept as recursiveOperationType
custom condition: true
rule {
  node<RuntimeTypeVariable> leftVar = binop.leftType as RuntimeTypeVariable; 
  node<RuntimeTypeVariable> rightVar = binop.rightType as RuntimeTypeVariable; 
  node<> leftType = null; 
  node<> rightType = null; 
if (leftVar.isNotNull) { 
  if (rightVar.isNotNull) { 
    // both unspecified 
    node<> inferredBoth = typechecker.getRulesManager().getOperationType(binop.binOperation, <to be inferred>, <to be inferred>); 
    if (inferredBoth.isNotNull) { 
      infer leftVar :<=: inferredBoth; 
      infer rightVar :<=: inferredBoth; 
      leftType = inferredBoth; 
      rightType = inferredBoth; 
    } else { 
      error "operator (" + binop.binOperation + ") does not have defined default operand types when both operands are to be inferred." -> equationInfo.getNodeWithError(); 
    } 
  } else { 
    // right is concrete 
    rightType = binop.rightType; 
    node<> inferredFromRight = typechecker.getRulesManager().getOperationType(binop.binOperation, <to be inferred>, rightType); 
    if (inferredFromRight.isNull) { 
      // try the same as opposite 
      node<> symmetricOperationType = typechecker.getRulesManager().getOperationType(binop.binOperation, rightType, rightType); 
      if (symmetricOperationType.isNotNull) { 
        inferredFromRight = rightType; 
      } 
    } 
    if (inferredFromRight.isNotNull) { 
      infer leftVar :<=: inferredFromRight; 
      leftType = inferredFromRight; 
    } else { 
      error "operator (" + binop.binOperation + ") does not have defined default left operand type (to be inferred) when the right operand is " + rightType -> equationInfo.getNodeWithError(); 
    } 
  } 
} else { 
  leftType = binop.leftType; 
  if (rightVar.isNotNull) { 
    // left is concrete 
    node<> inferredFromLeft = typechecker.getRulesManager().getOperationType(binop.binOperation, leftType, <to be inferred>); 
    if (inferredFromLeft.isNull) { 
      // try the same as opposite 
      node<> symmetricOperationType = typechecker.getRulesManager().getOperationType(binop.binOperation, leftType, leftType); 
      if (symmetricOperationType.isNotNull) { 
        inferredFromLeft = leftType; 
      } 
    } 
    if (inferredFromLeft.isNotNull) { 
      infer rightVar :<=: inferredFromLeft; 
      rightType = inferredFromLeft; 
    } else { 
      error "operator (" + binop.binOperation + ") does not have defined default left operand type (to be inferred) when the left operand is " + leftType -> equationInfo.getNodeWithError(); 
    } 
  } else { 
    rightType = binop.rightType; 
  } 
} 
if (leftType.isNotNull && rightType.isNotNull) { 
  // we have concrete binop type 
  // reported to JetBrains: node<> resultType1 = operation type(binop.binOperation, binop.leftType, binop.rightType); 
  node<> resultType = typechecker.getRulesManager().getOperationType(binop.binOperation, leftType, rightType); 
  if (resultType.isNotNull) { 
    // we can make this equal as the recursive type is only a "place holder" for reporting its concreteness 
    resultType :==: recursiveOperationType; 
    // infer resultType :<=: recursiveOperationType; 
  } else { 
    error "operator (" + binop.binOperation + ") is not supported for " + leftType + " and " + rightType -> equationInfo.getNodeWithError(); 
  } 
}
}
(in the code above is a workaraund of this reported bug MPS-19356)
I am using another trick-hack to be able to use the operator type(...) implementation to be able to infer the opposite types, or both operand types when needed. I've created another internal type ToBeInferred which can be used inside my overloaded operations rules. Here are some example rules:
operation concepts: LogicalAndExpr| LogicalOrExpr
left operand type: <bool> is exact: true
right operand type: <bool> is exact: true
operation type:
(operation, leftOperandType, rightOperandType)->node<> { 
  leftOperandType; 
}
-----------------------------------------------
operation concepts: LogicalAndExpr| LogicalOrExpr
left operand type: <bool> is exact: false use strong subtyping false
right operand type: <to be inferred> is exact: true
operation type:
(operation, leftOperandType, rightOperandType)->node<> { 
  // example of "pattern matching"-like operand type inference 
  // not needed in this case, but for the example; may be useful for non-symmetric overloadings 

  // infer from left 
  // the type is used as the inferred default operand type; the result type is defined by the fully specified rule 
  leftOperandType; 
}  
-----------------------------------------------
operation concepts: LogicalAndExpr| LogicalOrExpr
left operand type: <to be inferred> is exact: true
right operand type: <to be inferred> is exact: true
operation type:
(operation, leftOperandType, rightOperandType)->node<> { 
  // default operand is bool 
  // the type is used as the inferred default operand type; the result type is defined by the fully specified rule 
  <bool>; 
}                                                                                                                                                                          
So, operand types can be inferred via this extensible mechanism where one can specify the inferred type by pattern-matching-like rules plus a fall-back is used to try infer the operand type from the opposite operand when no such rule exist.

Now, I am happy again with my implementation, but it is still IMO a trick-hack solution, because what I actually would need is something like an "else" branch in the "when concrete" expression. Then the solution would be entirely in my typeof_BinaryExpr rule. Its main code fragments would look something like this (together with support for multi-arguments):
    when concrete (typeof(binaryExpr.leftExpr) as leftType, typeof(binaryExpr.rightExpr) as rightType) { 
 ... here we have both operands concrete, so a straightforward implementation ... 
    } else {
 ... here we have at least one of the operand as a variable ...
 ... which should be possible to check via an operation, for example, leftType.isTypeVariable, or isTypeVariable(leftType) ...
 ... the more complex logic similar to that of replace_binary_operation_type rule would go here ...
    }

Maybe, the semantics of the else branch would need some more design thinking to be correct (e.g., what to do with the concrete branch after the else is invoked? Or, should be the else branch invoked repeatedly when more and more arguments are becoming concrete?).
Anyway, I believe it is doable and it can make the type system more general and usable, specially for non-C-like languages.

Despite the problems that are still in the way, I am happy to use MPS for my pleasure and nurturing my hope that stone age of programming (I mean punch-cards-locked-in programming) is coming to an end (even writing this very comment is driving me and the Chrome browser crazy).