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.

On Wed, Jul 27, 2011 at 8:30 AM, Christopher Done wrote:

On 27 July 2011 13:58, Adam Chlipala wrote:

...

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?

Again I don't really know what you're talking about so I'll drop it.

Here's a question that I suspect may be relevant: Can you generate code with TH that isn't well-typed? If your first thought is something like "of course, how would you type check the code before generating it?", I would ask how that differs from "of course programs can crash, how can you check all inputs before reading them at run time?". Bonus question for any OCaml folks: What's the difference between using Camlp4 and using MetaOCaml? - C.