[Haskell-cafe] Free theorems for dependent types?

[Eugene Kirpichov]

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