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.
begin:vcard
fn:Joseph Fredette
n:Fredette;Joseph
adr:Apartment #3;;6 Dean Street;Worcester;Massachusetts;01609;United States of America
email;internet:[email protected]
tel;home:1-508-966-9889
tel;cell:1-508-254-9901
x-mozilla-html:FALSE
url:lowlymath.net, humbuggery.net
version:2.1
end:vcard
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
