[Ur] show t

[Adam Chlipala]

Gergely Buday wrote:
>>> $ 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.
>    

First, I should have noticed that [return] there, which we certainly 
don't want for a pure function.  ([txt] isn't typed as monadic, either.)

Second, now the problem is that [show_] doesn't have an explicit return 
type annotation, and, since the function is polymorphic, the compiler 
isn't confident of inferring a good type.  You can add [: page] to 
[show_] and it should work.

> 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?
>    

In order, they are form fields used and form fields defined.  The best 
documentation on the further details is the types of the tag combinators 
themselves, so, if you don't find them enlightening now, I suggest 
coming back to them after gaining more familiarity with the Ur type system.