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.
_______________________________________________ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
