[Ur] Ur/Web and document validation

[Adam Chlipala]

David LaPalomento wrote:
> I've been looking at statically typed, functional web programming
> tools and came across Ur/Web. One feature which struck me as
> particularly interesting was Ur's ability to ensure the generated HTML
> was always valid. I was curious, though, what criteria were being used
> to classify HTML as valid.
>    

Right now, the only checking has to do with grouping tags into sets of 
"contexts," where a tag may only be used in the proper context.  There 
are, in effect, a finite number of contexts (e.g., a table cell, regular 
body, etc.), which are implicit in the types of the tag combinators.  I 
haven't made any attempt to follow any specification of XHTML, and in 
fact I've never even read such a specification!  To me, this extra level 
of type detail is most useful as machine-checked documentation on what 
sorts of XHTML different functions/functors/etc. expect.