Re: [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 > 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@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [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  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  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@impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>
>
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur