On 27 July 2011 13:58, Adam Chlipala
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!