Christopher Done wrote:
On 19 July 2011 17:22, Adam Chlipala<ad...@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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
