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

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
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
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 ...)


Please sign in to leave a comment.