Type inference on guarded alternative

[luan-xiaokun]

Hey guys, I'm wondering how the type of a parse rule with guard is inferred. I found the following thing:

Modify the arithmetic example's rules as follows:

SimpleExpression:
    Addition<false>;

Expression:
    Addition<true>;

Addition<next> infers Expression:
    Multiplication<next> ({infer BinaryExpression.left=current} operator=('+' | '-') right=Multiplication<next>)*;

Multiplication<next> infers Expression:
    PrimaryExpression<next> ({infer BinaryExpression.left=current} operator=('*' | '/') right=PrimaryExpression<next>)*;

PrimaryExpression<next> infers Expression:
    '(' Expression ')' |
    {infer NumberLiteral} value=NUMBER |
    {infer FunctionCall} func=[AbstractDefinition] ('(' args+=Expression (',' args+=Expression)* ')')? |
    (<next> {infer NextExpression} 'next' '(' next=SimpleExpression ')');

A new kind of primary expression NextExpression is added, and expressions without next expressions are called simple expressions (at least this is what I intend to do).
I thought that the generated type for simple expression should not include next expression, but it turns out that export type SimpleExpression = Expression; is generated.

There are workarounds for this, but I think that this behavior is counterintuitive, is there something that I'm missing about guarded alternative? Or is this case too hard for type inference?

[msujew]

So in short, the type inference completely disregards alternative/group guards. I'm kind of curious what you are expecting as a generated type. The main issue here is that rules are transformed in isolation and not in the context of their calling rule. Especially since seem to expect that a rule is transformed into two distinct types, which is not really something which the current system is able to accomplish. And I believe this would be very hard to handle from a user perspective, as the amount of generated types is 2^n with n being the number of guard arguments in a rule. The only thing which I could reasonably imagine would be akin to something like:

type Expression<next extends boolean> = If<
    next, 
    NextExpression | NumberLiteral | ...,  // Keep `NextExpression` if `next` is true
    NumberLiteral | ... // omit the `NextExpression` if `next` is false
>;

However, that would lead to a few other issues, as we cannot determine during runtime which type it is, so the generated isExpression function can never tell whether next is true or false. This seems like a lot more trouble than it is worth.

[luan-xiaokun]

Thanks for your reply.

I'm kind of curious what you are expecting as a generated type.

I was expecting something like export type Expression = NextExpression | ... and export type SimpleExpression = .... But you are right, this may require walking through all rule calls, which can cause a high computation overhead.

I came up to this question when I was trying to develop a langium grammar for the model checker nuXmv's input language, and in some cases, the next operator is not allowed in expressions. Using group alternative is a solution, although the generated type for simple expression is not what I expected, it can still work pretty well.