4 Aug 15:03 1992

### Coherence and polymorphic instantiation

Date: Mon, 03 Aug 92 14:26:36 +0100 In the course of experimenting with adding some polymorphic constants to the second-order polymorphic lambda-calculus with subtyping (Fsub), we were led to wonder what kind of equational properties should be imposed to express compatibility between polymorphic instantiation and subtyping. To see the issue, consider the polymorphic type T = All(A) F(A) -> G(A) where both F and G are monotone type operators. If we have f:T, X<X', and x:F(X), then f can be applied to x in two ways: f [X] x f [X'] x We can now ask whether these two terms are equal elements of G(X') -- or more explicitly, whether [G(X) < G(X')] (f [X] x) = f [X'] ([F(X) < F(X')] x) : G(X') where [S<T] denotes the coercion from S to T. This equation holds trivially in untyped models and also, it seems, for definable polymorphic terms. It becomes interesting in typed(Continue reading)