[Haskell-cafe] Free theorems for dependent types?

[Eugene Kirpichov]

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.
>
> --
> Robin
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



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