On 10/08/2016 07:41 PM, Saulo Araujo wrote:
Thanks for suggesting this workaround. I was able to implement it, but
I have some doubts. [...]
After some trial and error, the compiler was happy with
con concat nm t r = [[nm] ~ r] => $([nm = t] ++ r)
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.
Oh, I was too quick to suggest my version without actually running it
through Ur/Web. Sorry about that.
[=>] 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)."
It looks like I might actually need to extend the parser to make your
example workable. Stay tuned....
Indeed, the compiler accepts
val fullName : concat #First string [Last = string] = fn [[First] ~
[Last = string]] => {First = "Saulo", Last = "Araujo"}
Surprisingly, however, besides fullName being a function, I can
manipulate it like a record
val first : string = fullName.First
Which reminds me of the Queen song "A Kind of Magic" :)
The type-inference engine automatically discards guards whose
constraints can be proved, so it isn't so magic after all. ;)
Sincerely,
Saulo
On Sat, Oct 8, 2016 at 2:05 PM, Adam Chlipala <[email protected]
<mailto:[email protected]>> wrote:
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!):
type blah x y z = $([x = y] ++ z)
... where type t = blah A.n1 A.t1 A.t2
It may need extra kind annotations.
On 10/07/2016 08:42 AM, Saulo Araujo wrote:
Hi,
I am trying to do something like
signature ARGUMENTS = sig
con n1 :: Name
con t1 :: Type
con t2 :: {Type}
constraint [n1] ~ t2
end
signature RESULT = sig
type t
end
functor Functor(A : ARGUMENTS) : RESULT where type t = $([A.n1
= A.t1] ++ A.t2) = struct
open A
type t = $([n1 = t1] ++ t2)
end
but the Ur/Web compiler complains saying:
test.ur:12:58: (to 12:60) syntax error: deleting CSYMBOL DOT
Parse failure
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?
Sincrely,
Saulo
_______________________________________________
Ur mailing list
[email protected] <mailto:[email protected]>
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
<http://www.impredicative.com/cgi-bin/mailman/listinfo/ur>
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
