Re: [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.



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Understanding Ur Inference Failure

[Adam Chlipala]

On 9/24/19 3:38 PM, Mario Alvarez wrote:
The idea behind the function is the following: I want to construct a 
record by combining together a record representing a set of 
customization options with a record representing a set of defaults.

[...]
fun recDif' [ts1 ::: {Type}] [ts2 ::: {Type}] [ts3 ::: {Type}] [ts1 ~ 
ts2] [ts2 ~ ts3] [ts1 ~ ts3]
           (fl : folder (ts2)) (r1 : $(ts1 ++ ts2)) (r2 : $(ts2 ++ 
ts3)) : $(ts1) =
    @fold [fn ts2 => ts1 ::: {Type} -> [ts1 ~ ts2] => $(ts1 ++ ts2) -> 
$(ts1)]

     (fn [nm ::_] [v ::_] [r ::_] [[nm] ~ r]
                  (f : ts1 ::: {Type} -> [ts1 ~ r] => $(ts1 ++ r) -> 
$(ts1))

[ts1] [ts1 ~ [nm = v] ++ r] (z : $(ts1 ++ ([nm = v]) ++ r)) =>
            f (z -- nm))
     (fn [ts1] [ts1 ~ []] (r : $(ts1 ++ [])) => r) fl ! r1

fun mergeDfl [more ::: {Type}] [overlap :: {Type}] [rest ::: {Type}]
    [more ~ overlap] [overlap ~ rest] [more ~ rest] (fl : folder overlap)
    (i1 : $(more ++ overlap)) (i2 : $(overlap ++ rest)) : $(more ++ 
overlap ++ rest) =

    (i1 ++ (@recDif' ! ! ! fl i2 i1))


Have you seen the triple-minus operator [---]?  I think it does your 
[recDif'], without the seemingly superfluous parameters.  You could 
replace the last line above with [i1 ++ (i2 --- overlap)].


Writing [recDif'] does seem to have been a useful exercise in Ur/Web 
metaprogramming!  Congrats on entering the elite club of people who have 
written new folds from scratch. >:)



I then attempt to run both of these functions on some simple examples:
[...]
val fails = mergeDflInfer {A = 1, B = 1} {B = 2, C = 3}
[...]
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:35: (to 191:51) Error in 
final record unification

Can't unify record constructors
Have:  [A = int, B = int]
Need:   ++ 


In general, Ur inference isn't meant to solve equalities with just 
multiple unification variables concatenated together on one side.  You 
should always set things up so that there is at most one unification 
variable left when we get to unifying record types.  The underlying 
type-inference problem is undecidable, so we're fundamentally limited to 
using heuristics, and your case here didn't come up before to motivate a 
heuristic to support it.



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] Understanding Ur Inference Failure

[Mario Alvarez]

Dear Ur Users,

I've written a function in Ur that typechecks, but that Ur's inference
appears to fail on unless I explicitly specify type-parameters.

The idea behind the function is the following: I want to construct a record
by combining together a record representing a set of customization options
with a record representing a set of defaults.

I have a record type (overlap ++ rest) representing the defaults, and
another record type (more ++ overlap) representing the customizations. The
idea is that the "more" and "overlap" fields will be taken from the
customization parameter, the "rest" fields will be taken from the default
parameter, and the result will be of type (more ++ overlap ++ rest).

I have implemented this as the following, using record folds to define a
helper function "recDif" that calculates the "rest" part of the defaults
parameter, given the customization and defaults.

Note that I define two versions of mergeDfl, one which expects the overlap
to be given explicitly as a type parameter, and the other which attempts to
infer it. Otherwise the two versions are identical.

--

fun recDif' [ts1 ::: {Type}] [ts2 ::: {Type}] [ts3 ::: {Type}] [ts1 ~ ts2]
[ts2 ~ ts3] [ts1 ~ ts3]
   (fl : folder (ts2)) (r1 : $(ts1 ++ ts2)) (r2 : $(ts2 ++ ts3)) :
$(ts1) =
@fold [fn ts2 => ts1 ::: {Type} -> [ts1 ~ ts2] => $(ts1 ++ ts2) ->
$(ts1)]
 (fn [nm ::_] [v ::_] [r ::_] [[nm] ~ r]
  (f : ts1 ::: {Type} -> [ts1 ~ r] => $(ts1 ++ r) -> $(ts1))
[ts1] [ts1 ~ [nm = v] ++ r] (z : $(ts1 ++ ([nm = v]) ++ r)) =>
f (z -- nm))
 (fn [ts1] [ts1 ~ []] (r : $(ts1 ++ [])) => r) fl ! r1

fun mergeDfl [more ::: {Type}] [overlap :: {Type}] [rest ::: {Type}]
[more ~ overlap] [overlap ~ rest] [more ~ rest] (fl : folder overlap)
(i1 : $(more ++ overlap)) (i2 : $(overlap ++ rest)) : $(more ++ overlap
++ rest) =
(i1 ++ (@recDif' ! ! ! fl i2 i1))

fun mergeDflInfer [more ::: {Type}] [overlap ::: {Type}] [rest ::: {Type}]
[more ~ overlap] [overlap ~ rest] [more ~ rest] (fl : folder overlap)
(i1 : $(more ++ overlap)) (i2 : $(overlap ++ rest)) : $(more ++ overlap
++ rest) =
(i1 ++ (@recDif' ! ! ! fl i2 i1))

--

I then attempt to run both of these functions on some simple examples:

-

val works = mergeDfl [[B = int]] {A = 1, B = 1} {B = 2, C = 3}
val fails = mergeDflInfer {A = 1, B = 1} {B = 2, C = 3}

---

If we run the first version of merged ("mergeDfl"), supplying the "overlap"
type parameter as follows, UrWeb accepts it ("val works"). However, if we
run the second modified version of merged ("mergeDflInfer") and attempt to
force UrWeb to infer the overlap ("val fails"), UrWeb rejects it with the
following error:

--

/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:35: (to 191:51) Error in final
record unification
Can't unify record constructors
Have:  [A = int, B = int]
Need:   ++ 
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:35: (to 191:51) Stuck unifying
these records after canceling matching pieces:
Have:  [A = int, B = int]
Need:   ++ 
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:25: (to 191:34) Error in final
record unification
Can't unify record constructors
Have:  [A = int]
Need:   ++ 
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:25: (to 191:34) Stuck unifying
these records after canceling matching pieces:
Have:  [A = int]
Need:   ++ 
yorix@DESKTOP-84OVJN9:~/winhome/Code/Lunes$ urweb lunes
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:41: (to 188:55) Error in final
record unification
Can't unify record constructors
Have:  [B = int, C = int]
Need:   ++ 
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:41: (to 188:55) Stuck unifying
these records after canceling matching pieces:
Have:  [B = int, C = int]
Need:   ++ 
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:26: (to 188:40) Error in final
record unification
Can't unify record constructors
Have:  [A = int, B = int]
Need:   ++ 
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:188:26: (to 188:40) Stuck unifying
these records after canceling matching pieces:
Have:  [A = int, B = int]
Need:   ++ 

--

Is Ur's inference algorithm simply unable to infer the overlap in a
situation like this, or am I doing something wrong? I am using Ur version
20190217.

Best,
Mario Alvarez
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur