[Haskell-cafe] Ur tutorial, and a challenge

[Adam Chlipala]

Christopher Done wrote:
> On 19 July 2011 17:22, Adam Chlipala<adamc at impredicative.com>  wrote:
>    
>>     http://www.impredicative.com/ur/demo/crud1.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)?
>>      
> Is TemplateHaskell fair game?

Sure.

> Because if so these problems are not hard.

Maybe, but I don't think you've outlined any solutions that meet my 
criteria.  The key property is what I've highlighted in my self-quote 
above: the challenge is to type-check _the_code_generator_, not just the 
individual programs it generates.  I want a static theorem that every 
program coming out of the code generator will play by the rules.  Even 
rules that are trivial to check for individual programs (e.g., no code 
injection attacks because you follow a simple AST discipline) become 
quite non-trivial when you are reasoning about the behavior of a code 
generator.  Also, this "simple" property gets more interesting when you 
also want to enforce statically, e.g., that all SQL queries are 
type-correct w.r.t. the database.

> Yesod employs static typing for templates.

Does this static type system support metaprogramming strong enough to 
implement my challenge problem with the level of static guarantee for 
all specialization parameters that I ask for?

> HaskellDB achieves
> injectionless static type checking even without TemplateHaskell

Right.  Easy to do for individual programs, harder to do for a code 
generator.

> and templatepg has type safe SQL queries based on parsing the SQL itself
> and inspecting the types involved by asking the PostgreSQL server
> directly at compile time.

Ur/Web does this, too, as a kind of belt-and-suspenders measure.  This 
alone provides no support for static checking of metaprograms.