[Haskell-cafe] Ur tutorial, and a challenge

[Christopher Done]

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