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 <ad...@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@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