[Ur] Understanding Ur Inference Failure

[Mario Alvarez]

Hi Adam,

Thanks for your reply! I appreciate the tip about [---]; I think I had seen
it while looking through the Ur manual but for some reason didn't think it
was what I wanted. It definitely is, though.

I also appreciate the encouragement about writing custom folds: it was
challenging to understand what was going on, but I found the second part of
your tutorial on Ur to be an extremely useful resource in trying to figure
out how to do it. The ability to do type-level programming of the kind
described in that tutorial is part of what drew me to Ur.

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'm guessing based on your response that the answer is no; I
just want to be sure. Especially if nobody else is doing this kind of thing
with Ur, I definitely don't expect you to change Ur's heuristics just to
handle this case, especially if doing so would worsen performance on other
tasks :)

In the meantime, I've found that I can get a slightly less general version
of a similar thing to work: I can write

--------------

fun mergeDflWeak [overlap ::: {Type}] [rest ::: {Type}]
    [overlap ~ rest]
    (i1 : $(overlap)) (i2 : $(overlap ++ rest)) : $(overlap ++ rest) =
    (i1 ++ (i2 --- overlap)

--------------

and inference for this works fine, although it leaves out the possibility
of having the first argument extend the record with additional fields.
Still, it may be sufficient for my purposes since I can make the "defaults"
parameter contain all fields that I might possibly want to add on later.

Thanks again for your help.

--Mario


On Tue, Sep 24, 2019 at 1:05 PM Adam Chlipala <adamc at csail.mit.edu> wrote:

> 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:  <UNIF:U235::{Type}> ++ <UNIF:U234::{Type}>
>
> 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 at impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20190924/c042348b/attachment-0001.html>