monotonic subtype relations?
Date: Wed, 10 Apr 91 10:38:53 EST
One of my students (David Wright) is looking at type inference including
needed reduction information (see Tapsoft 1991). An interesting feature of
the work is that there is a 'subtype' relation that is naturally covariant
in the sense that a leq a' & b leq b' implies a->b leq a'->b'. (The usual
implication is that a'->b leq a->b'.)
It would seem to follow that the 'simple semantics' is inappropriate
for this type system. I (we) would appreciate any pointers to any relevant
papers that readers may be aware of that may help us develop the 'right'
semantics, or indeed, any references to work involving such monotonic type
relations. Suggestions most welcome.
Clem Baker-Finch AARNet: firstname.lastname@example.org
Information Sciences & Engineering Phone: +61 6 2522408
University of Canberra Fax: +61 6 2522191
PO Box 1, Belconnen
A.C.T. Australia 2616