[Haskell-cafe] Ur tutorial, and a challenge

[Adam Chlipala]

Last week, I posted a message to this list looking for people interested 
in joining projects using my domain-specific language Ur/Web.  Some 
responses rightly chastised me for the lack of documentation on the core 
Ur language's novel type system features.  I'm sure many Haskellers have 
had the experience of quickly grokking the interfaces of new libraries 
by reading their type signatures, and I think the same is true for Ur.  
So, to provide that initial bump of background that should help folks 
get started, I've begun an Ur tutorial:
     http://www.impredicative.com/ur/tutorial/
The chapters that are already there are intended to be sufficient to 
help any experienced Haskell programmer get started quickly with 
Ur/Web.  In particular the second chapter on type-level programming may 
be of interest as a mind expander, even for folks who don't want to use 
Ur/Web.

I'd love feedback about weaknesses in the tutorial!

I also want to attach a challenge to this tutorial, as an expansion to 
an answer I gave earlier about why Ur/Web needs a new programming 
language and can't just be implemented as a Haskell library.  Consider 
this online Ur/Web demo:
     http://www.impredicative.com/ur/demo/crud1.html
The example involves a library component encapsulating functionality 
like that of Ruby on Rails's scaffolding: automatic generation of a 
standard web-based "admin interface" to an SQL database table.  The 
Ur/Web version uses static typing to guarantee that any applications 
generated by this component are free of injection attacks and other 
generic problems.  The guarantees apply both to app communication with 
server-side pieces (e.g., static type-checking of SQL) and client-side 
pieces (e.g., static type-checking of HTML).  This is not done by 
type-checking individual invocations of the admin-interface component.  
Rather, the component is checked at a static type which guarantees 
correct operation for _any_specialization_parameters_.

So, the challenge is, can this functionality be implemented in Haskell 
(GHC extensions fair game, any web framework allowed)?  If so, how 
pretty is it? :)