On 27 July 2011 13:58, Adam Chlipala <ad...@impredicative.com> wrote: > 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.
No, I didn't outline any solutions for that criteria. I'm not competent to answer that. >> 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? Again I don't really know what you're talking about so I'll drop it. Agda is still on my list of things to learn. As is Ur. But that order seems appropriate. Ciao! _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
