Re: [Haskell-cafe] Ur tutorial, and a challenge

Christopher Done wrote:

On 19 July 2011 17:22, Adam Chlipala 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.