[Haskell-cafe] Free theorems for dependent types?

[Joe Fredette]

This word has piqued my interest, I've hear it tossed around the 
community quite a bit, but never fully understood what it meant. What 
exactly is a 'free theorem'?

Eugene Kirpichov wrote:
> Hello,
>
> 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?
>
> This seems very promising to me for the following reason: Take the
> free theorem for 'sort::(a->a->Bool)->[a]->[a]'. The theorem could
> possibly be a lot more powerful if there were a way to encode in the
> type of 'sort' that it accepts a reflexive transitive antisymmetric
> predicate, but the only way to express that is with dependent types.
>
> Looks like the only thing one needs to add to System F is the
> relational translation rule for a dependent product; but I haven't
> tried doing it myself.
>
>   
-------------- next part --------------
A non-text attachment was scrubbed...
Name: jfredett.vcf
Type: text/x-vcard
Size: 296 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20090517/1206f280/jfredett.vcf