[TYPES] polymorphic isomorphisms

[Paul B Levy]

Dear all,

Do the following System F isomorphisms appear in the literature, and 
are they validated by the standard models?

(1)

Prod X. ((X -> B) -> A) cong A [ nu X. B / X ]
where X is negative in A and positive in B

(2)

Prod X. ((B -> X) -> A) cong A [ mu X. B / X ]
where X is positive in A and B

Also, are any other isomorphisms (beyond the obvious beta-eta ones) known? 
(By "isomorphism" I mean definable both ways by terms that are inverse up 
to observational equivalence.)

The following isomorphisms are similar, but they're already derivable from 
(1)-(2).

(3)

Sum X. ((X -> B) x A) cong A [ nu X. B / X ]
where X is positive in A and B

(4)

Sum X. ((B -> X) x A) cong A [ mu X. B / X ]
where X is negative in A and positive in B

regards,
Paul



-- 
Paul Blain Levy              email: pbl at cs.bham.ac.uk
School of Computer Science, University of Birmingham
Birmingham B15 2TT, U.K.      tel: +44 121-414-4792
http://www.cs.bham.ac.uk/~pbl