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