Type - Subtype relation. Something seems unclear

Question

I'm reading some slides of a class on object oriented programming languages and stepped into the type-subtype definition:

Barbara Liskov, “Data Abstraction and Hierarchy,” SIGPLAN Notices, 23,5 (May, 1988):

What is wanted here is something like the following substitution property: If for each object o_s of type S there is an object o_T of type T such that for all programs P
defined in terms of T, the behavior of P is unchanged when o_S is substituted for o_T then S is a subtype of T

Then it goes with an example:

Point = { x:Integer, y:Integer }
PositivePoint = { x:Positive, y:Positive }
where Positive = { k:Integer | k > 0 }

Can we say that PositivePoint ≤ Point?

Yes, because an element of type PositivePoint may always replace an element of type Point in a program defined in Point terms!

Now... for me it seems it should be quite the opposite: Point ≤ PositivePoint because I couldn't use PositivePoint in a program that uses Point with negative coordinates, while I could to the opposite.

I doubted if the syntax was Type ≤ Sub-type or Sub-Type ≤ Type, but the statement seems more clear, what's wrong then?

---

Edit

Just to make things easier the question is: Can you say that PositivePoint is a subtype of Point? Why?

---

2nd Edit

I report here what I wrote in a comment hoping it will make my problem clearer:

Suppose that the program has to draw a square map from Point (-100, -100) to Point (100, 100). What would happen if you use type PositivePoint? Would the program's behavior be unchanged? It would not. This "unchanged behavior" is the only thing I don't get. If the definition of subtype was simply inheriting and overriding from an other type it would be ok, but it doesn't seem to be the case.

Answer 1

You can model the type relationships through subsets.

PositivePoint ⊂ Point holds for the same reason as PositiveInt ⊂ Int does: Positive numbers are a subset of all possible numbers!

Every PositivePoint belongs to the Points, but not other way round.

Answer 2

I haven't seen the ≤ symbol used to denote this before, but what I think is meant by PositivePoint ≤ Point means that Point has a greater range of potential values than PositivePoint (i.e.: PositivePoint is a subset of Point, all instances of PositivePoint could be replaced by a valid instance of Point, but not the other way around.)

Answer 3

The idea is that any function which accepts a PositivePoint relies on the fact that the point's values are positive. If you passed in a Point whose values are not positive, the assumption is false and the function would fail.

A function accepting a Point, however, would make no assumptions about the point's positiveness, so if you passed in a PositivePoint, it would be fine.

Note that this is only true for an immutable Point class. If you were able to change a Point's value, PositivePoint and Point could be in no subclass relationship at all because the operation p.x = -1 would fail for PositivePoints.

Edit: To elaborate:

Let's say we have 2 dimensional array which automatically grows when required (i.e. you never get an index-out-of-bounds error when passing two positive indices). Now we have a function which accepts a PositiveInteger p and then accesses the 2d-array at index x,y. This can't fail because x and y are guaranteed to be positive and the 2d-array can be indexed with any pair of positive indices. However if Point was a subtype of PositivePoint, p could actually have negative values even though it's declared to be positive. This would mean that it's no longer safe to use it to index the array.

However a function accepting a Point doesn't know whether the point's values are negative or positive - it already has to take into account the possibility that they're positive. So passing in a PositiveInteger can't break anything.

Answer 4

Liskov is correct, PositivePoint ≤ Point, because PositivePoint is a refinement of Point. Any code that uses Point must also be able to use PositivePoint, because there was always the possibility that Point's coordinates were positive anyway. The reverse is not true, because code using PositivePoint may act under the assumption that the coordinates are always positive, and replacing PositivePoint with Point would break that assumption.

Note that she's not saying that a PositivePoint can replace a Point, just that a PositivePoint can be used where a Point is needed.