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

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.

Answer 2

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.