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 <[email protected]>: > On Sun, 17 May 2009 23:10:12 +0400 > Eugene Kirpichov <[email protected]> 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
