<div dir="ltr">Hi Adam,<div><br></div><div>Thanks for suggesting this workaround. I was able to implement it, but I have some doubts. Perhaps you can point me to the relevant bits in the Ur/Web documentation or you can clear them up.</div><div><br></div><div>Following your suggestion, I started defining</div><div><br></div><div>con concat nm t r = $([nm = t] ++ r)<br></div><div><br></div><div>But the Ur/Web compiler complains</div><div><br></div><div><div>test.ur:1:22: (to 1:37) Couldn't prove field name disjointness</div><div> Con 1: [nm = ()]</div><div> Con 2: r</div><div>Hnormed 1: [nm = ()]</div><div>Hnormed 2: r</div></div><div><br></div><div>I tried to please the compiler by changing the definition to</div><div><br></div><div>con concat nm t r [[nm] ~ r] = $([nm = t] ++ r)<br></div><div><br></div><div>Now, the compiler complains:</div><div><br></div><div><div>test.ur:5:12: (to 5:14) Invalid FFI mode</div><div>test.ur:5:15: (to 5:16) Invalid FFI mode</div><div>test.ur:5:17: (to 5:18) Invalid FFI mode</div><div>test.ur:5:0: (to 5:4) syntax error: replacing LTYPE with VAL</div><div>test.ur:5:12: (to 5:14) Invalid FFI mode</div><div>test.ur:5:15: (to 5:16) Invalid FFI mode</div><div>test.ur:5:17: (to 5:18) Invalid FFI mode</div><div>test.ur:5:30: (to 5:31) syntax error: replacing EQ with LBRACK</div><div>test.ur:16:0: (to 16:0) syntax error found at EOF</div><div>Parse failure</div></div><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. 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><br></div><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="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 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/c<wbr>gi-bin/mailman/listinfo/ur</a><br>
</blockquote></div><br></div>