This question relates to liskov substitution principle seems to have two conventional meanings but is really a different question, so I'm posing it as a new question.
I'm doing a bit of research into an old language, Common Lisp, which defines function-type as follows:
f is of type
(function (A) Y) if every call
(f x) is semantically equivalent to
(the Y (f (the A x))).
the" is a special operator which specifies that the value returned by the form is of the specified type.
My question is whether this definition of function-type is enough to derive subtype rules, and type intersection/union/complement rules?
For example if
f is both
(function (A) Y) and simultaneously of type
(function (B) X), then can we say from the definition that
f is of type
(function ((and A B)) (and Y X)), or perhaps can we say that it is
(function ((or A B)) (and X Y))?
The language (specified in the mid 1980s) specifies that the intersection rule, but not the complement nor the union rules. The intersection of two function types is the former
(function ((and A B)) (and Y X)), which might surprise some people. I'm wondering
- Whether this intersection rule follows from the definition?
- Whether the rule is a contradiction?
- Can we also derive the complement and union rules from the definition?
- Can we derive a subtype rule? I.e., if
(function (A) Y), then
fis also in
(function (B) X)if ...what....?
With regard to (4) we would like to say that if $Y \subset X$ and $B \subset A$, then $(A\to Y) \subset (B\to X)$, but that would violate the intersection rule.