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




_______________________________________________
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

Reply via email to