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

The overloading relation * ~ * is defined by *f:t _{1} ~ f:t_{2}*
iff there is a type

Equivalence of expansions is defined only w.r.t. the
* < ^{ -> }* relation.

- Allow a covariant extension of the
__<__^{ -> }*t*and_{1}__<__^{ -> }t_{2}*u*implies_{1}__<__^{ -> }u_{2}*[t*. 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_{1}--> ° u_{1}]__<__^{ -> }[t_{2}--> ° u_{2}]*t*and_{1}*t*(as well as_{2}*u*and_{1}*u*) to have common supersorts and use a restriction of the graph.)_{2}The problem with this is that it is incompatible with the

__<__^{ => }__<__^{ => }-expressions instead.__\__ - An orthogonal question is whether we should allow arbitrary
many-one embeddings by allowing the user
to contribute explicitly to the
__<__^{ => }

CoFI Note: L-8 ---- 7 January 1998.

Comments to till@informatik.uni-bremen.de