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