Variants, subtyping

Posted-Date: Sat, 11 Mar 89 21:31 EST
Date: Sat, 11 Mar 89 21:31 EST

In fact, the inconsistency mentioned in the previous messages follows already
>from VARIANT and

       f(case t g h)  =  case t (g;f) (h;f)  .

Also, the latter equation yields STRONG VARIANT in the presence of

       case t inleft inright  =  t  .

Regarding the coalesced sums of domains, note that e.g. for Scott domains
these coalesced sums are coproducts in the subcategory of strict maps.
Also, a separated sum of domains  A  and  B  is just the coalesced sum
of the "lifted" domains  Abottom  and Bbottom.  Now this lifting is the
left adjoint to the inclusion of the subcategory of strict maps into the
category of continuous maps, i.e. the subcategory is "reflective".
The same holds for linear vs. stable maps of Girard's coherent spaces.
[All this is from the Breazu-Tannen, Coquand, Gunter & Scedrov paper
on inheritance and explicit coercion.]  So in some sense variants
still are coproducts, but in a reflective subcategory.

Now while Val was speaking at MIT, two of his cohorts at Penn were busily
verifying the naturality conditions on strict (linear, resp.) maps needed for
the validity of the subtyping rule for positive recursion [the rule Val
mentioned in his talk].  Let me assume that in the rule suggested by O'Toole
a is not free in t and likewise b is not free in s .  Then the rule is valid
in the domain-theoretic semantics, but I don't see that it includes the
subtyping rule for positive recursion.  Presumably a calculus with both rules
is valid in domain-theoretic semantics, but we're still checking that.