[Ur] Understanding Ur Inference Failure

[Adam Chlipala]

On 9/24/19 4:54 PM, Mario Alvarez wrote:
> Finally, a quick follow-up question: is there any way to convince the 
> Ur inference engine as it currently stands to solve this kind of 
> problem? (For instance, would it be possible to write a type-level 
> function to compute the overlap between the records in my example, or 
> would this just lead to a different version of the same unification 
> problem that the inference engine can't solve?)

I don't know a way to write it in today's Ur/Web, and let me try to 
explain why it is a big departure from existing features, to contemplate 
an extended unification approach.

Faced with a unification like [[A = int] = U1 ++ U2], it is ambiguous 
how to split the record literal among the two unification variables [U1] 
and [U2].  We could try both possibilities, but that would require 
backtracking to undo unification decisions.  As in classic ML type 
inference, Ur/Web's engine never backtracks past variable assignments.  
So we seem to need some unification approach that looks at multiple 
unsolved constraints at once, to make better choices.  Again, it is a 
fundamental design decision in both ML type inference and Ur/Web's to 
consider one unification constraint at a time, communicating between 
them only through side effects to assign values to unification variables.