Replacement Rule not applying "in time"

I am noticing that some typesystem rules have an odd precedence to others.

An example program :
`class Top`
`class Bottom extends Top`

`fun <X extends Top, Y extends X> foo(arg: Y) : X = arg` ---- foo takes an argument of type Y and has a return type of X

// `::foo` indicates a reference to the function foo
`fun thisWorksAsExpected(): Bottom = ::foo.invoke(new Middle())` ---- In this case, the type of `::foo` is correctly inferred to be `(Bottom) -> Bottom` due to inference from `invoke`
`fun hereLiesTheIssue() : (Bottom -> Bottom) = ::foo` ---- In this case, inference breaks down, the explanation is below
There’s many typesystem rules w/ a lot of inference that goes into making this work, but I’ll explain the fundamental issue I’m seeing

Given this, when the typesystem has finished evaluating rules, I end up with three inequalities.
*note*: lower-case letters indicate a typesystem type, and in our typesystem a function type appears as `(args…) -> return`:

*State before solving inequalities*
`(s) -> r` <= `(Bottom) -> Bottom` --- This is an inequation comparing two function types, the left-hand side is the type of the function reference, the right-hand side is the return type
`r` <= `Top` ---- `r` is the typesystem type corresponding to TypeParameter `X`, the inference rule is derived from its’ bound
`s` <= `r`---- `s` is tye typesystem type corresponding to TypeParameter `Y`, its bound is X thus we end up with this rule.
The top inequation should trigger a ReplacementRule for function types (using contravariance for arguments and covariance for return). If this were evaluated, the state would become:

*Expected state after replacement rule*
`s >= Bottom`
`r <= Bottom`
`r` <= `Top`
`s` <= `r`
This would lead to the correct types being applied - both `r` and `s` would be `Bottom`

However the latter two are evaluated before the first leading to invalid behavior.
`r` and `s` end up being inferred as `Top`, which leads to an invalid comparison:

*Actual state when solved*
`Top -> Top` <= `Bottom -> Bottom`

Is it possible to indicate that the replacement rule should apply first? If not, how should this be implemented?

edit: also notice that markdown is not supported here :(


So, the problem seems to be that the particular rule (an inequation replacement rule) doesn't apply when you expect it. The issue here is that the order, in which rules are applied, is not specified by the semantics of type inference engine, and there are reasons for that. But there might be a way to solve your problem if you do away with type inference where it’s enough to check the constraints.

Here’s what is happening, as I see it, when your problematic code is analysed.

First, parameters X and Y are processed, which adds inequalities s <= Top and r <= s. Then an inequality involving two function types is added. This system of inequalities is then solved for variables s and r, and only then “replacement rules” are processed. I assume this is in accordance with your observations as well.

But what if there were no inequalities involving s and r in the first place? What is the reason for the constraints on type parameters to be used in type inference? Isn’t it enough if these constraints are only “checked”? So, instead of adding an “infer” type inequation you could add a “when concrete” block and *check* if the types are correct.

I hope this helps.



Thanks for your reply!

In our case, we actually do perform a lot of inference. For example, given the following program:

  NOTE: The following is a property of our language, not of this program. I wanted to state it for clarity.
 *typedef number = real
 *typedef integer = natural
 *integer :<=: number

function foo(a: Set<SomeClass>): integer = {
  let val = sum(a, (it) => it.getSomeIntegerValue())
return val + 5

function <A extends AnyClass, B extends number> sum(set: Set<A>, sumFunc: (A) => B) : B = set.fold(0, (it, accum) => accum + sumFunc.invoke(it))

There is a lot of inference happening to make foo such a simple function.

  • "let val" - variable types are inferred based on their right-hand-side. Also, in some cases, they are inferred based on their usage. This example doesn't necessarily reflect that use case, but I could come up with an example of such.
  • "sum(...)" - There is a *lot* of inference happening here. The type parameters A and B are inferred based on the arguments passed to sum. Additionally, this is where a rule comparing the lambda's function type to the function's expected parameter type is added.
  • "(it) => it.getSomeIntegerValue()" - The lambda's type is not known at declaration time, it is effectively "(tv1) => tv2" (tv = type var). The type of "it" is inferred based on the context in which the lambda is used. The concrete typevar of A is eventually bound to `SomeClass` for this invocation. Additionally, the function's return type is inferred based on the type of its body.

In many other cases, this works exactly as expected. We are thorough about adding inference rules where necessary, and we are comfortable with the fact that there may be *some* user programs that have indeterminate type. Those will likely be very rare, and there are always options to provide static types to assist the type engine.

However, this fails in some situations when the Function <: Function comparison does not invoke the replacement rule before other assumptions have been made.

Given our typesystem, we avoid `when concrete` whenever possible as it prevents inference from working properly. We haven't been able to successfully replace Operator types with inference yet, but I have some ideas around using meet/join types to turn overloads into inference rules. In those few cases, however, using user-defined types solves the problem (and is acceptable). We had previously used a shallow when-concrete to facilitate function type comparison, though this was replaced in favor of the replacement rule as that when-concrete would've needed to be present for *any* inference that could have contained function types.



May I inquire why is my suggestion to replace inference with checking on already calculated types does not work for you?

Also, when it comes to higher order functions, one has to be very careful in order to not make the typesystem undecidable. I'm afraid the inference rules for your language can be broken fundamentally, as I couldn't not re-create a working sample with this logic in either Kotlin or Java 8, both of which have very strong type inference. 

As to the original issue, there is very little we can do at the moment, save for rewriting the inference engine with new semantics, which would likely break compatibility with all the typing rules written so far by all of our clients. 



Please sign in to leave a comment.