MPS Typesystem: Explicit Pull-up vs Push-down constraints
In our language we often run into a use case where a given type variable has both upper and lower bounds.
Given variable `a`, these bounds might be declared as such:
a :<=: ClassType(SomeClass)
a :>=: BottomClassType
In these cases, MPS occasionally behaves nondeterministically depending on the complexity/shape of the surrounding program, resolving either to the upper or lower bound (however it seems to generally prefer the lower bound). In this case, given that the lower bound is a fairly unspecified/useless type for a function argument, we would prefer to resolve to the upper bound.
I am fairly familiar with Kotlin's typesystem and the fact that it provides a way to resolve ambiguities using pull-up and push-down rules, as defined here: https://kotlinlang.org/spec/kotlin-type-constraints.html#finding-optimal-constraint-system-solution
Does MPS provide any functionality like this? If not, is there any way to help resolve this ambiguity manually? It is quite a frustrating issue as it makes fairly obvious inference into a bit of a debugging nightmare.
Please sign in to leave a comment.
Hi! I don't think any pull up or push down functionality is offered by the type system currently.
As you observed, the lower bound is always preferred, but sometimes the upper bound is selected. I believe the reason for that is the type system engine would try to solve your constraints before all of them are applied to your type variables (when all rules remaining in the solver are "when concrete", the type system tries to assign a type to them in order to move forward and that could skip further rules from being applied to the final type).
In your example it would give three different situations :
I believe this kind of race condition cannot really be solved at the moment without changing the current type system engine (and it would also be the first obstacle to implement pull up/push down constraints).
However, in case you would only have one upper bound and one lower bound, and the pull up / push down is requested only once (or a known amount of all of those when the type rule of the node to be inferred is triggered), I may have some workaround to offer you.
The idea would be to have some "pullable wrapper type", which would be given to your inferred node (or replacing your type variable). This type would wrap lower and upper bound, plus a indicator to know if the resolution would be pull up or pull down.
Then a replacement rule could decide, when the pull direction is concrete, which bound to use for subtyping.
While this could help with simple cases (one upper and lower bound), this may be problematic for unknown amount of upper, lower bounds or pull-up / push-down "requests", as the same race condition described above could occur and alter the computation. In case that seems interesting to you, I pushed the sample project I made at https://github.com/cdelabou/mps-pull-constraint.