17 May
2009
17 May
'09
7:10 p.m.
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. -- Eugene Kirpichov Web IR developer, market.yandex.ru