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
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
