how to deduce a function subtype rule from a given function type definition

Question

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: An object 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

1. Whether this intersection rule follows from the definition?
2. Whether the rule is a contradiction?
3. Can we also derive the complement and union rules from the definition?
4. Can we derive a subtype rule? I.e., if f is in (function (A) Y), then f is 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.

Answer 1

The intersection rule should be derivable, but it isn't purely a subtyping rule. Basically we reason as follows (I've translated into a notation that's a bit more familiar to me):

• I'm presuming that subtyping says $A \cap B \subseteq A \subseteq A \cup B$
• Subtyping means that $f : (A \to Y) \cap (B \to X)$ leads to both $f : A \to Y$ and $f : B \to X$
• If $f : A \to Y$, it is then the case that $x : A ⊢ f \; x : Y$. But subtyping $A \cap B \subseteq A$ means that $x : A \cap B ⊢ f \; x : Y$ follows.
• The same argument means that $f : B \to X$ leads to $x : A \cap B ⊢ f \; x : X$
• These two judgments together lead to $x : A \cap B ⊢ f \; x : X \cap Y$
• This leads back to $f : A \cap B \to X \cap Y$

Another way to specify this is that $f : (A \to X) \cap (A \to Y)$ leads to $f : A \to X \cap Y$. Subtyping allows us to broaden the original $A$ and $B$ to the common $A \cap B$, and then apply this intersection rule. But the intersection rule isn't subtyping, it is the rule for deducing that something has an intersection type via two separate deductions.

Pure subtyping can allow you to go from $f : A \to Y$ to $f : A \cap B \to X \cup Y$. Note that this is refining the input and broadening the output, and we could do each individually.

For union types, there is an opposite sort of rule. $f : (A \to Y) \cap (B \to Y)$ leads to $f : A \cup B \to Y$. So, if you can map both $A$ values and $B$ values to $Y$ values, you can map their union to $Y$ values. However, note that this doesn't allow us to deduce your rule with a union. Instead, we can only get from $f : (A \to Y) \cap (B \to X)$ to $f : A \cup B \to X \cup Y$, because this time we can broaden the result type of both functions and apply the union rule.

But, there is no way (I think) to get to $f : A \cup B \to X \cap Y$, which makes sense if you think about it. Just because we know that $f$ takes $A$ values to $Y$ values and $B$ values to $X$ values doesn't imply that it takes all $B$ values to $Y$ values and $A$ values to $X$ values, which is what that specification says.

So, to sum up:

1. The rule is derivable (with some standard assumptions, I think).
2. The rule is not a contradiction.
3. We can derive a union rule, but not the one you wrote. And I'm unsure what 'complement' rule you're talking about.
4. Subtyping works as usual, but it is not the only basis for the intersection/union rules.

Edit: Here's a summary of the rules that I believe hold, as I think it might lead you less astray than the long stuff above:

$$(A \to Y) \cap (B \to X) \subseteq (A \cap B) \to (X \cap Y)$$ $$(A \to Y) \cap (B \to Y) \cong A \cup B \to Y$$ $$(A \to X) \cap (A \to Y) \cong A \to X \cap Y$$

In particular, note that the first relationship is subtyping, not equivalence. The intersection of the function types carries more information than the function between intersection types. If the lisp documentation you're looking at says those are the same, it's wrong. Consider, just because we know that a function takes $A \cap B$ to $X \cap Y$ doesn't tell us anything about what it takes $A - B$ to. However, if it's merely saying that knowing $f$ has the first two types, we can conclude it also has the third type, that is correct.