Go backward to 6 Predicate types
Go up to Top
Go forward to 8 \-abstraction
7 Subsorting
Design proposal:
Introduce two subsorting relations < -> and
< => . < -> is the standard subsorting
relation, extended to higher-order types
covariantly in the second argument of the function
space constructors. The semantics of < ->
is as in the first-order case.
< => is an extension of < -> ,
acting contravariantly in the first argument
of the function space constructors.
The semantics is a (non-injective) coercion
which can be obtained by a restriction of
functions to a smaller domain.
Since we loose injectivity, we loose the possibility
of casting to a < => -subtype.
The extension of the two
subsorting relations to product types and partial types
is straightforward. Total function types
are < -> than the corresponding partial
function types. For predicate types,
we have that t1 < => t2 implies
t2 => truth < => t1 => truth.
The overloading relation ~ is defined by f:t1 ~ f:t2
iff there is a type t with t1,t2 < => t.
By contravariancy of < => in the first
argument of function and predicate space constructors,
this extends the first-order overloading relations ~ F and
~ P.
Equivalence of expansions is defined only w.r.t. the
< -> relation.
Alternatives:
- Allow a covariant extension of the < -> ordering,
by setting t1 < -> t2 and u1 < -> u2 implies
[t1 --> ° u1] < -> [t2 --> ° u2].
The intuition would be to inject a function
from the smaller into the larger function space
by using the function with the same graph.
(It would even suffice just to require
t1 and t2 (as well as u1 and u2) to have
common supersorts and use a restriction of the graph.)
The problem with this is that it is incompatible with
the < => -ordering, since triangles of injections
(well, with < => , not all "injections" are really
injective)
do no longer commute.
Therefore, to obtain these
coercions, we propose to use \-expressions instead.
- An orthogonal question is whether we should allow arbitrary
many-one embeddings by allowing the user
to contribute explicitly to the < => relation.
CoFI
Note: L-8 ---- 7 January 1998.
Comments to till@informatik.uni-bremen.de