<div dir="ltr">Thanks for the new year's gift Adam! :)<div><br></div><div>Happy new year you all,</div><div>Saulo<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Dec 31, 2016 at 4:51 PM, Adam Chlipala <span dir="ltr"><<a 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">
<div bgcolor="#FFFFFF" text="#000000">
<div class="m_8319393102651142217moz-cite-prefix">OK, after much anticipation... I
finally made the Ur/Web grammar change that should make your
original code Just Work.<div><div class="h5"><br>
<br>
On 10/12/2016 01:50 PM, Adam Chlipala wrote:<br>
</div></div></div><div><div class="h5">
<blockquote type="cite">
On 10/08/2016 07:41 PM, Saulo Araujo wrote:<br>
<blockquote 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 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 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 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="m_8319393102651142217h5"><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>
</div>
</div>
</blockquote>
</div>
</div>
</blockquote>
</blockquote>
<br>
</div></div></div>
<br>______________________________<wbr>_________________<br>
Ur mailing list<br>
<a href="mailto:Ur@impredicative.com">Ur@impredicative.com</a><br>
<a href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" rel="noreferrer" target="_blank">http://www.impredicative.com/<wbr>cgi-bin/mailman/listinfo/ur</a><br>
<br></blockquote></div><br></div>