[Haskell-cafe] Free theorems for dependent types?
jfredett at gmail.com
Sun May 17 22:51:38 EDT 2009
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:
> 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...
Size: 296 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20090517/1206f280/jfredett.vcf
More information about the Haskell-Cafe