[TYPES] CPO semantics of recursive types
Malcolm Tyrrell
Malcolm.Tyrrell at computing.dcu.ie
Fri Oct 27 08:42:27 EDT 2006
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.
More information about the Types-list
mailing list