
24 Oct
2011
24 Oct
'11
2:30 a.m.
On 2011-10-23 17:02:47 -0700, Brandon Moore said:
It sounds like the entire point of this is syntax representation?
Not really...... the entire point of this is parametricity. :) There are a lot of examples involving syntax and binding because ruling out exotic terms is one of the things that parametricity is really useful for.
If so, have you seen Conor McBride's recent post http://www.e-pig.org/epilogue/?p=773
Yes, a while back; it's very cool but basically orthogonal: the data types in that blog post aren't indexed by the object-language-term's type (nor should they be -- he's writing a typechecker, after all!). - a