Re: [Haskell-cafe] Free theorems for dependent types?

I'm glad that someone is doing research in that direction! Are your results so far applicable to create a free theorem for that example with sortBy? 2009/5/17 Robin Green :

On Sun, 17 May 2009 23:10:12 +0400 Eugene Kirpichov 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

-- Eugene Kirpichov Web IR developer, market.yandex.ru