[Ur] XML records from higher-order type classes

[Benjamin Barenblat]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

On Thursday, April  9, 2015, at  8:28 pm EDT, Adam Chlipala wrote:
> In Ur, types and values are in different namespaces.  The [a] near the 
> end is a different [a] from the one bound as a formal argument!  In 
> particular, it is resolving to the <a> tag from the standard library.

Ah, how funny.  vanila was just talking about that exact problem on IRC.

Anyway, I’m now stuck with another error:

- ---8<-----------------cut here----------------start--------------->8----
structure Container : sig
    class container :: (Type -> Type) -> Type
    val inject : a ::: Type -> f ::: (Type -> Type)
                 -> container f
                 -> a -> f a
end = struct
    con container f = {Inject : a ::: Type -> a -> f a}
    fun inject [a] [f] witness x = witness.Inject x
end
- ---8<-----------------cut here----------------end----------------->8----

gives

    container.ur:8:4: (to 8:51) Error in final record unification
    Can't unify record constructors
       Have:  <UNIF:G::{Type}> ++ [Inject = a -> f a]
       Need:  [Inject = a ::: Type -> a -> f a]
      Field:  #Inject
    Value 1:  a -> f a
    Value 2:  a ::: Type -> a -> f a
    Incompatible constructors
    Have:  a -> f a
    Need:  a ::: Type -> a -> f a

so I tried making the type parameter explicit:

- ---8<-----------------cut here----------------start--------------->8----
structure Container : sig
    class container :: (Type -> Type) -> Type
    val inject : a ::: Type -> f ::: (Type -> Type)
                 -> container f
                 -> a -> f a
end = struct
    con container f = {Inject : a :: Type -> a -> f a}
    fun inject [a] [f] witness x = witness.Inject [a] x
end
- ---8<-----------------cut here----------------end----------------->8----

But that gives

    container.ur:8:35: (to 8:49) Expression is not a constructor function
    Expression:  witness.#Inject
          Type:  <UNIF:F::Type>

What does ‘Expression is not a constructor function’ mean?

Thanks,
Benjamin
-----BEGIN PGP SIGNATURE-----

iQF8BAEBCgBmBQJVJxvIXxSAAAAAAC4AKGlzc3Vlci1mcHJAbm90YXRpb25zLm9w
ZW5wZ3AuZmlmdGhob3JzZW1hbi5uZXQ5OThCQjVEMTlDOEE3QjE3OUUwREFCODY5
RTczMDE0OUVCOTFDNTNCAAoJEJ5zAUnrkcU7Mq8IALV9ssj2eLyMCie6UpsdLFJS
MmHMc5XTAgXVb1OPX8ZusTMCuweBpE0YCDZD/34UsQSBgjddvTL2xmxQo35EWkxz
eTrlPQTNxHaLKgi2Q5281/mjKBlGv7BO7d0SyJJdGQWn+uSurkyd423My8y3CzZU
JEeaykEoWGA5zORq8Lth7T82yTqJZw0KjzFdNSTS3A+E8HSFutHhnyvBvcFMd9vB
PYEiBuYFRYx7lVpX5da/3hnzs4ENGmTXz2ygrkrz3wmgklYGLrft7qX5BB0OEcJR
B9Crvys+fofLDumrHMRWuTQxRQYXjkJJQtkcV356U+IUi50LXGj62XWOInn4I30=
=UYLz
-----END PGP SIGNATURE-----