🚀 go-pugleaf

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
models, however, when polymorphic constants are added.  For example,
if we add a base type Bool and a constant

    if : All(A) Bool->A->A->A

then it seems natural to require that:

          b : Bool   X < X'    x1, x2 : X 
    -----------------------------------------
    (if [X] b x1 x2) = (if [X'] b x1 x2) : X'

More generally, we might require that *every* well-typed equation
whose type-erasure is a syntactic identity should hold in the typed
model.  This is stronger than the usual coherence condition, which
only addresses differences in denotations arising from different ways
of reconstructing coercions in a single explicitly typed term.

We wonder whether this stronger sort of coherence property has ever
been considered in the literature, or whether there are reasonable
examples for which it would be undesirable.  (It seems that such a
situation could only arise in a non-parametric model.)

        Martin Hofmann
        Benjamin Pierce