[Ur] show t

[Gergely Buday]

>> $ cat bar.ur
>> fun show_ [t] (arg : show t) =
>>     return<xml>{[arg]}</xml>
>>
>
> Something is already strange with this definition, so I suggest fixing that
> first and seeing if the problem recurs.  The code above tries to show the
> witness of membership in the type class [show].  What you want instead is to
> use that witness to render a particular value of type [t].  You probably
> meant this:
>
> fun show_ [t] (_ : show t) (arg : t) =
>    return <xml>{[arg]}</xml>
>
> BTW, this function is already in the standard library and is present in the
> default context, with the name [txt], with a more general type.

fun main () = return ( txt "Hello World!" )

works with the mentioned [txt] function, but not with the rewritten
show_ . How can I express that the t type is a member of the show
typeclass? My original goal was to write a function that is able to
compare two arbitrary values using the show function.

And let me have another question about the xml type constructor, like in:

val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []

ctx seems to be the opening html tag(s), as obvious from the following
definitions:

con xhtml = xml [Html]
con page = xhtml [] []
con xbody = xml [Body] [] []
con xtable = xml [Body, Table] [] []
con xtr = xml [Body, Tr] [] []
con xform = xml [Body, Form] [] []

But what is the semantics of the other two implicit kind parameters?

- Gergely