[Haskell-cafe] Free theorems for dependent types?
ekirpichov at gmail.com
Sun May 17 15:48:27 EDT 2009
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 <greenrd at greenrd.org>:
> On Sun, 17 May 2009 23:10:12 +0400
> Eugene Kirpichov <ekirpichov at 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
Web IR developer, market.yandex.ru
More information about the Haskell-Cafe