17 May
2009
17 May
'09
7:41 p.m.
On Sun, 17 May 2009 23:10:12 +0400
Eugene Kirpichov
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?
Yes. I did some research into it as part of my master's thesis, the final version of which is not quite ready yet. Basically, free theorems in the Calculus of Constructions can be substantially more complicated, because they have to exclude certain dependent types in order to be valid. So much so that I do not think that they are necessarily worthwhile to use in proofs. But that is just an intuition, and I have not done enough different kinds of proofs to state this with any confidence. -- Robin