[Prev][Next][Index][Thread]

# Re: monotonic subtype relations?

• To: types
• Subject: Re: monotonic subtype relations?
• From: John.Reynolds@proof.ergo.cs.cmu.edu
• Date: Wed, 10 Apr 91 12:38:51 EDT
• In-Reply-To: Your message of Tue, 09 Apr 91 22:31:22 -0400. <9104100231.AA01926@stork>
• In-Reply-To: Your message of Tue, 09 Apr 91 22:31:22 -0400. <9104100231.AA01926@stork>
• Sender: meyer@theory.lcs.mit.edu

```To: Clem Baker-Finch <clem@echo.canberra.edu.au>
Cc: types@theory.lcs.mit.edu
Date: Wed, 10 Apr 91 10:02:34 EDT

In Dana Scott's work, there are several notions of "subdomain" that may
fit your needs.  A retraction pair <f,g> from a domain D to a domain E
consists of continuous functions f from D to E and g from E to D
such that f;g is the identity on D. (I use semicolons for composition
in diagrammatic order.)  If g;f approximates the identity on E, then
the retraction pair is called a projection pair; if the identity on E
approximates g;f then the retraction pair is called a closure pair.

If <f,g> is a retraction (projection, closure) pair from D to E and
<f',g'> is a retraction (projection, closure) pair from D' to E' then
<f",g"> is a retraction (projection, closure) pair from D->D' to E->E',
where f"(h) = g;h;f' and g"(h) = f;h;g'.

Thus one could give a semantics to a subtyping relation where -> is
monotonic in both arguments by using a functor from the preorder of
types to the category of retraction pairs (or either of its subcategories
of projection or closure pairs).  Informally, one interprets "a is a
subtype of b" as "There is a retraction pair from the domain denoted by a
to the domain denoted by b".

I hope this helps. -- John Reynolds

```