<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
On 10/08/2016 07:41 PM, Saulo Araujo wrote:<br>
<blockquote
cite="mid:CA+ckhoTTGpGpDNMrLb9cizzV8-rMJ7bETK+aEuho8KbgrEJJsA@mail.gmail.com"
type="cite">
<div dir="ltr">Thanks for suggesting this workaround. I was able
to implement it, but I have some doubts. [...]
<div><br>
</div>
<div>After some trial and error, the compiler was happy with</div>
<div><br>
</div>
<div>con concat nm t r = [[nm] ~ r] => $([nm = t] ++ r)<br>
</div>
<div><br>
</div>
<div>Which brings me the question: what is [[nm] ~ r] =>
$([nm = t] ++ r)? Besides from the "=>" token, it looks
like the type of a function that produces a record from a
disjointness proof.</div>
</div>
</blockquote>
<br>
Oh, I was too quick to suggest my version without actually running
it through Ur/Web. Sorry about that.<br>
<br>
[=>] is a guard, saying "you only get a value of this type (to
the right of the arrow) if you can prove this constraint (to the
left)."<br>
<br>
It looks like I might actually need to extend the parser to make
your example workable. Stay tuned....<br>
<br>
<blockquote
cite="mid:CA+ckhoTTGpGpDNMrLb9cizzV8-rMJ7bETK+aEuho8KbgrEJJsA@mail.gmail.com"
type="cite">
<div dir="ltr">
<div>Indeed, the compiler accepts</div>
<div><br>
</div>
<div>val fullName : concat #First string [Last = string] = fn
[[First] ~ [Last = string]] => {First = "Saulo", Last =
"Araujo"}<br>
</div>
<div><br>
</div>
<div>Surprisingly, however, besides fullName being a function, I
can manipulate it like a record</div>
<div><br>
</div>
<div>val first : string = fullName.First</div>
<div><br>
</div>
<div>Which reminds me of the Queen song "A Kind of Magic" :)</div>
</div>
</blockquote>
<br>
The type-inference engine automatically discards guards whose
constraints can be proved, so it isn't so magic after all. ;)<br>
<br>
<blockquote
cite="mid:CA+ckhoTTGpGpDNMrLb9cizzV8-rMJ7bETK+aEuho8KbgrEJJsA@mail.gmail.com"
type="cite">
<div dir="ltr">
<div>Sincerely,</div>
<div>Saulo</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Sat, Oct 8, 2016 at 2:05 PM, Adam
Chlipala <span dir="ltr"><<a moz-do-not-send="true"
href="mailto:adamc@csail.mit.edu" target="_blank">adamc@csail.mit.edu</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">It does
seem likely that the parser isn't allowing qualified names
in record literals. The problem is easy to work around by
defining a type synonym that you use instead. Here's some
code (not actually run through Ur/Web yet!):<br>
type blah x y z = $([x = y] ++ z)<br>
... where type t = blah A.n1 A.t1 A.t2<br>
It may need extra kind annotations.
<div>
<div class="h5"><br>
<br>
On 10/07/2016 08:42 AM, Saulo Araujo wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi,<br>
<br>
I am trying to do something like<br>
<br>
signature ARGUMENTS = sig<br>
con n1 :: Name<br>
con t1 :: Type<br>
con t2 :: {Type}<br>
constraint [n1] ~ t2<br>
end<br>
<br>
signature RESULT = sig<br>
type t<br>
end<br>
<br>
functor Functor(A : ARGUMENTS) : RESULT where type t =
$([A.n1 = A.t1] ++ A.t2) = struct<br>
open A<br>
<br>
type t = $([n1 = t1] ++ t2)<br>
end<br>
<br>
but the Ur/Web compiler complains saying:<br>
<br>
test.ur:12:58: (to 12:60) syntax error: deleting
CSYMBOL DOT<br>
Parse failure<br>
<br>
Apparently, one cannot construct type-level records by
projecting name variables from a module. Is this a
grammar/parser bug? If so, is there a workaround?<br>
<br>
Sincrely,<br>
Saulo<br>
</blockquote>
<br>
</div>
</div>
______________________________<wbr>_________________<br>
Ur mailing list<br>
<a moz-do-not-send="true" href="mailto:Ur@impredicative.com"
target="_blank">Ur@impredicative.com</a><br>
<a moz-do-not-send="true"
href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur"
rel="noreferrer" target="_blank">http://www.impredicative.com/c<wbr>gi-bin/mailman/listinfo/ur</a><br>
</blockquote>
</div>
<br>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Ur mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Ur@impredicative.com">Ur@impredicative.com</a>
<a class="moz-txt-link-freetext" href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a>
</pre>
</blockquote>
<br>
</body>
</html>