Discussion of "overload" feature in K and whether to support it

The legacy Haskell backend implements a constructor "overloading" feature described in a long design document, for a particular kind of overloading.
The booster backend does not currently support this functionality, and the cost-benefit relation is questionable, as we discuss here using the motivating example from the design document.

module NUMBERS-SYNTAX
    imports INT-SYNTAX
    imports FLOAT-SYNTAX

    syntax IValType ::= "i32" | "i64"
    syntax FValType ::= "f32" | "f64"
    syntax AValType ::= IValType | FValType
    syntax Number ::= Int | Float
    syntax IVal ::= "<" IValType ">" Int    [klabel(<_>_)]
    syntax FVal ::= "<" FValType ">" Float  [klabel(<_>_)]
    syntax  Val ::= IVal | FVal
    // the problematic constructor:
    syntax  Val ::= "<" AValType ">" Number [klabel(<_>_)]
endmodule

With this syntax, the K compiler will identify the last constructor < _ > _ : ValType -> Number -> Val as a kind of "super-constructor" overloaded by both the FVal and IVal constructor:

• all three have the same klabel
• all three have the same arity
• both the argument types and the result types are in a subsort relationship (FValType,IValType < ValType, Float,Int < Number, FVal, IVal < Val).

NB This is a very specific case of "overloading", which generally would allow for different arities and has no relation to subsorting per se.

Equations are generated which amount to

< inj{FValType, ValType}(vt) > inj{Float, Number}(f) #Equals inj(FVal,Val}(<vt > f // using FVal constructor
< inj{IValType, ValType}(vt) > inj{  Int, Number}(i) #Equals inj(IVal,Val}(<vt > i // using IVal constructor

Now, when unifying Values from a rule LHS and from the input (subject), a problem arises:

module NUMBERS
    imports NUMBERS-SYNTAX
    imports INT
    imports FLOAT
    imports MAP

    rule [problem]: <k> (0 |-> <i32> IValue) => 0 |-> f(IValue) </k> // with an opaque f : Number -> Val for illustration

This rule won't match against a concrete singleton map 0 |-> <i32> 1 (which uses the IVal constructor, because of the existence of the indeterminate Val constructor (which is required for the "overloading" mechanism implemented).
(this issue came up in private code using a real-world semantics)

The legacy backend kore-rpc implements complicated logic to apply the generated equations (right-to-left) and insert appropriate injections to align the rule LHS and the subject. An additional complication here is that the Map will contain keys and values injected from their original sort to KItem and the injection chains are shortened.

Note that the rule LHS already contains a literal i32. Therefore it is clear that IValue is supposed to be of sort Int but the rule's RHS does not determine this sort. More generally, the following function demonstrates that the Val-sorted constructor enables creating ill-defined Values (clearly f32 and f64 should not be used for the ValType when the Number is in fact of sort Int and vice-versa with i32, i64.

    // creates ill-formed values
    syntax Val ::= creature32 ( Number ) [function, total]
    rule creature32(I:Int) => <f32> I
    rule creature32(F:Float) => <i32> F

The fix for the rule in question would be to just constrain IValue:Int to be of sort Int, thereby determining the constructor used in the rule's LHS. Likewise, if the RHS were to imply this sort for IValue we would know the constructor is that of IVal.

However, this raises the more general question of whether the overloading functionality is useful at all. The motivating example has some implicit invariants that the top-most constructor violates.

If we were to simply remove the problematic Val ::= "<" AValType ">" Number, the creature32 function above would not type-check any more. On the flip-side, ad-hoc polymorphic functions would have to be more verbose:

    syntax Number ::=- retract ( Val ) [ function, total]
    rule retract(< _ > N) => N // "ambiguous parse" of IVal or FVal constructor
endmodule

One would have to write a separate rule for each of the constructors. In this case it would be sufficient to add a :Int and :Float at the end in (two copies of) the rule above

It is unclear whether this convenience justifies the complexity of the overload unification implemented in the legacy unifier.

Start with the linked overloaded-constructors design document and the motivating NUMBERS-SYNTAX example. Read the legacy kore-rpc unifier's handling of generated equations and injection chains, then compare it with the booster backend. Done means reaching and documenting a decision on whether to support this overload behavior and what scope that support would require.