[TYPES] CPO semantics of recursive types

[Malcolm Tyrrell]

Thanks to all those who replied (on and off list). As I feared,
recursive domain equations do not, in general, have solutions in the
monotonic case.  I'm working with a typed functional language in
which the domain D = D->D is unlikely to arise. However, losing
recursive types altogether would be very annoying.

One very interesting suggestion (thanks!) was to use a smaller space
for [T->U], such as the space of kappa-continuous functions. I will
investigate this in due course.

Can anyone suggest how other specification languages, which support
recursive types, overcome this problem?

For the moment, I will adopt a defensive position and disallow
recursive types where the recursion parameter occurs in either
argument of a function type constructor. I expect that this
restriction is stronger than necessary (at least, I hope it is). I
also expect (hope!) that the significant majority of types used in
practice will satisfy the condition.  Certainly, standard types such
as lists, trees, etc. would be OK.

Unfortunately, I can think of an important example which the
restriction excludes, namely objects. For example, the following ML
datatype would be disallowed:

(**
  * A type for Point objects.
  *)
datatype Point = Point of {
   getX : int,           (* the x coordinate *)
   getY : int,           (* the y coordinate *)
   setX : int -> Point,  (* set the x coordinate *)
   setY : int -> Point,  (* set the y coordinate *)
   eq   : Point -> bool, (* does this point equal another point? *)
   add  : Point -> Point (* add another point to this point *)
}

(I just hacked up this simple object encoding for this posting, so
it may not be the best representative of the problem.)

Malcolm.