[Ur] Grammar/Parser bug?

[Saulo Araujo]

Thanks for the new year's gift Adam! :)

Happy new year you all,
Saulo

On Sat, Dec 31, 2016 at 4:51 PM, Adam Chlipala <adamc at csail.mit.edu> wrote:

> 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> 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
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20161231/633e0b91/attachment.html>