On Sun, 17 May 2009 23:10:12 +0400 Eugene Kirpichov <ekirpic...@gmail.com> wrote:
> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe