Subtyping for Recursive Types

       (1) During his presentation, Val mentioned some results that the
           simply-typed \-calculus, with ``strong variants'' and recursive
           types has an inconsistent equational logic.

   Can anyone tell me what this means?  What are strong variants, for
   example?
-------------
Strong variants are to surjective pairing what variants are to pairing.

PAIRING:  left(pair(x,y))=x, right(pair(x,y))=y
VARIANT:  case (lnleft x) f g = f x, and case(inright y) f g = g y

SURJECTIVE-PAIRING:  [pairing]  and [pair(left p, right p)=p]
STRONG-VARIANT: [variant] and  [case s (h o inleft) (h o inright) = h s]

Strong variants are what a category theorist would call a ``sum'' or
``coproduct''.

The theorem Val mentioned (attributed to Lawvere, but formulated in a way
more accessible to Computer Scientists in a forthcoming paper in TCS by Huwig
and Poigne), is that if you take lambda calculus over ANY set of types closed
under --> with the usual (eg beta) axioms and rules, PLUS fixed point (i.e.,
Y x = x (Y x) ) and strong variant axioms at enough types, then the system is
equationally inconsistent: one can prove M=N for ALL terms M,N of the same
type.

With recursive types one can derive fixpoints by simulating the untyped
lambda calculus self-applicative fixed point combinators, so strong variants
and recursive types are also inconsistent.

For example, cpo domains of course have fixed points.  So although they have
more than one useful variant-like construction, viz., separated sums and
coalesced sums, no cpo constructor can be a categorical sum.  In particular,
if + is the cpo separated sum, then + is a variant, but the strong variant
equation fails for s=bottom_(A+B) and any NON-STRICT h:A+B-->A+B.

Your other remarks about subtyping recursive types sound fascinating, and I
look forward to reading the responses of other TYPES subscribers.

Regards, A.