[Haskell-cafe] Free theorems for dependent types?
greenrd at greenrd.org
Sun May 17 15:41:02 EDT 2009
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.
More information about the Haskell-Cafe