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:

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

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