This word has piqued my interest, I've hear it tossed around the community quite a bit, but never fully understood what it meant. What exactly is a 'free theorem'? Eugene Kirpichov wrote:
Hello,
Is there any research on applying free theorems / parametricity to type systems more complex than System F; namely, Fomega, or calculus of constructions and alike?
This seems very promising to me for the following reason: Take the free theorem for 'sort::(a->a->Bool)->[a]->[a]'. The theorem could possibly be a lot more powerful if there were a way to encode in the type of 'sort' that it accepts a reflexive transitive antisymmetric predicate, but the only way to express that is with dependent types.
Looks like the only thing one needs to add to System F is the relational translation rule for a dependent product; but I haven't tried doing it myself.