[Ur] Grammar/Parser bug?

[Adam Chlipala]

OK, after much anticipation... I finally made the Ur/Web grammar change 
that should make your original code Just Work.

On 10/12/2016 01:50 PM, Adam Chlipala wrote:
> 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
>>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20161231/944f93e3/attachment.html>