Subtyping for Recursive Types

To: james@zermatt.lcs.mit.edu
Subject: Subtyping for Recursive Types
From: meyer@theory.LCS.MIT.EDU
Date: Sat, 11 Mar 89 13:48:50 EST
Cc: types@theory.LCS.MIT.EDU
In-Reply-To: James William O'Toole Jr.'s message of Sat, 11 Mar 89 09:47:18 EST <8903111447.AA02550@stork.LCS.MIT.EDU>

       (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.