[Ur] Grammar/Parser bug?

[Saulo Araujo]

Hi Adam,

Thanks for suggesting this workaround. I was able to implement it, but I
have some doubts. Perhaps you can point me to the relevant bits in the
Ur/Web documentation or you can clear them up.

Following your suggestion, I started defining

con concat nm t r = $([nm = t] ++ r)

But the Ur/Web compiler complains

test.ur:1:22: (to 1:37) Couldn't prove field name disjointness
    Con 1:  [nm = ()]
    Con 2:  r
Hnormed 1:  [nm = ()]
Hnormed 2:  r

I tried to please the compiler by changing the definition to

con concat nm t r [[nm] ~ r] = $([nm = t] ++ r)

Now, the compiler complains:

test.ur:5:12: (to 5:14) Invalid FFI mode
test.ur:5:15: (to 5:16) Invalid FFI mode
test.ur:5:17: (to 5:18) Invalid FFI mode
test.ur:5:0: (to 5:4) syntax error: replacing  LTYPE with  VAL
test.ur:5:12: (to 5:14) Invalid FFI mode
test.ur:5:15: (to 5:16) Invalid FFI mode
test.ur:5:17: (to 5:18) Invalid FFI mode
test.ur:5:30: (to 5:31) syntax error: replacing  EQ with  LBRACK
test.ur:16:0: (to 16:0) syntax error found at EOF
Parse failure

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. 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" :)

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/20161008/2e802bc8/attachment.html>