[Ur] Grammar/Parser bug?

[Adam Chlipala]

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 <adamc at csail.mit.edu 
> <mailto:adamc at csail.mit.edu>> 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
>     Ur at impredicative.com <mailto:Ur at impredicative.com>
>     http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>     <http://www.impredicative.com/cgi-bin/mailman/listinfo/ur>
>
>
>
>
> _______________________________________________
> Ur mailing list
> Ur at impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20161012/9be3a461/attachment.html>