when concrete over sequence of types


I am trying to implement a typesystem for my language. This worked so far for the simpler cases, but I am having some trouble with typing a construct that depends on the types of all of it's children, and there can be any amount of children ([0..n]). Each of the children can have one of three types: T1, T2 or T3<subtype1,subtype2,...>. I want to establish the following rules:

1: If any of the children have type T3, then the result is this type, and all other children with type T3 must have exactly the same subtypes.

2: if any of the children have type T2, then the result is T2, and none of the other children can have type T3

3: in all other cases, the result type is T1

The main problem I am facing is that the types of all the children have to be at least shallowly concrete before I can determine the return type, but there does not seem to be any language construct that does this. the "when concrete" syntax only allows for one node at a time, and nesting them is only possible if the amount of nodes is some predefined number. I am relatively new to MPS, so it is entirely possible that there is an obvious solution, but I am not seeing it. 

Any help would be appreciated.



a when_concrete on a sequence of size n is implemented in typechecking rule for method invocation. It's not exactly straightforward, but doable. The idea is that when_concrete blocks are executed in a loop, and "last" one to be executed (not necessarily the last in the original sequence) triggers the computation of the resulting type. You'd probably need to keep a queue of types that are still to be computed, shared between those blocks. 

Having said that, I wonder how is this scheme going to work at all, because I believe the 1. above contradicts the 2. And I assume by "subtypes" you mean type parameters. 

In case you are experimenting with your language and looking for an alternative way to describe the typesystem, you may want to take a look at Coderules: https://github.com/JetBrains/mps-coderules. This feature is experimental and you should expect some hacking around in order to make it work for you, but I'd be happy to assist and answer any questions you may have, 





Thanks for your reaction. I looked at some of the method call concepts in base language, but none of those seemed to follow this pattern as far as I could see. I ended up making each of the when concrete bodies call an inference method on an object with a counter. The counter is set to the amount of variables to check, and decreased every time the method is called. If it reaches zero, the final return type code is executed. This seems to work, but it also looks like it would be prone to race conditions if the when concrete blocks are executed in a multithreaded fashion. I don't know if this is a problem, or what I could do to prevent it if it is. 

There is no problem in the type rules, although I might not have written them down clearly. If both rule 1 and rule 2 apply this is a type error, so they can contradict each other on the return type. With subtypes I did indeed mean the type parameters.

I feel like I have already implemented at least 80% of the typesystem using the regular MPS type inference rules, so I don't really feel like starting again using a different framework. It might be interesting for any future projects though.


Please sign in to leave a comment.