<div dir="ltr"><div>Hi Adam,<br><br></div><div>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.<br><br></div><div>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.<br><br></div><div>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 :)<br><br></div><div>In the meantime, I've found that I can get a slightly less general version of a similar thing to work: I can write<br><br>--------------<br><br>fun mergeDflWeak [overlap ::: {Type}] [rest ::: {Type}]<br> [overlap ~ rest]<br> (i1 : $(overlap)) (i2 : $(overlap ++ rest)) : $(overlap ++ rest) =<br> (i1 ++ (i2 --- overlap)<br><br>--------------<br><br></div><div>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.<br></div><div><br></div><div>Thanks again for your help.</div><div><br>--Mario<br></div><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 24, 2019 at 1:05 PM Adam Chlipala <<a href="mailto:adamc@csail.mit.edu">adamc@csail.mit.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 9/24/19 3:38 PM, Mario Alvarez wrote:<br>
> The idea behind the function is the following: I want to construct a <br>
> record by combining together a record representing a set of <br>
> customization options with a record representing a set of defaults.<br>
> [...]<br>
> fun recDif' [ts1 ::: {Type}] [ts2 ::: {Type}] [ts3 ::: {Type}] [ts1 ~ <br>
> ts2] [ts2 ~ ts3] [ts1 ~ ts3]<br>
> (fl : folder (ts2)) (r1 : $(ts1 ++ ts2)) (r2 : $(ts2 ++ <br>
> ts3)) : $(ts1) =<br>
> @fold [fn ts2 => ts1 ::: {Type} -> [ts1 ~ ts2] => $(ts1 ++ ts2) -> <br>
> $(ts1)]<br>
> (fn [nm ::_] [v ::_] [r ::_] [[nm] ~ r]<br>
> (f : ts1 ::: {Type} -> [ts1 ~ r] => $(ts1 ++ r) -> <br>
> $(ts1))<br>
> [ts1] [ts1 ~ [nm = v] ++ r] (z : $(ts1 ++ ([nm = v]) ++ r)) =><br>
> f (z -- nm))<br>
> (fn [ts1] [ts1 ~ []] (r : $(ts1 ++ [])) => r) fl ! r1<br>
><br>
> fun mergeDfl [more ::: {Type}] [overlap :: {Type}] [rest ::: {Type}]<br>
> [more ~ overlap] [overlap ~ rest] [more ~ rest] (fl : folder overlap)<br>
> (i1 : $(more ++ overlap)) (i2 : $(overlap ++ rest)) : $(more ++ <br>
> overlap ++ rest) =<br>
> (i1 ++ (@recDif' ! ! ! fl i2 i1))<br>
<br>
Have you seen the triple-minus operator [---]? I think it does your <br>
[recDif'], without the seemingly superfluous parameters. You could <br>
replace the last line above with [i1 ++ (i2 --- overlap)].<br>
<br>
Writing [recDif'] does seem to have been a useful exercise in Ur/Web <br>
metaprogramming! Congrats on entering the elite club of people who have <br>
written new folds from scratch. >:)<br>
<br>
> I then attempt to run both of these functions on some simple examples:<br>
> [...]<br>
> val fails = mergeDflInfer {A = 1, B = 1} {B = 2, C = 3}<br>
> [...]<br>
> /mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:35: (to 191:51) Error in <br>
> final record unification<br>
> Can't unify record constructors<br>
> Have: [A = int, B = int]<br>
> Need: <UNIF:U235::{Type}> ++ <UNIF:U234::{Type}><br>
<br>
In general, Ur inference isn't meant to solve equalities with just <br>
multiple unification variables concatenated together on one side. You <br>
should always set things up so that there is at most one unification <br>
variable left when we get to unifying record types. The underlying <br>
type-inference problem is undecidable, so we're fundamentally limited to <br>
using heuristics, and your case here didn't come up before to motivate a <br>
heuristic to support it.<br>
<br>
<br>
_______________________________________________<br>
Ur mailing list<br>
<a href="mailto:Ur@impredicative.com" target="_blank">Ur@impredicative.com</a><br>
<a href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" rel="noreferrer" target="_blank">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br>
</blockquote></div></div>