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

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.

• I've not understood the precise semantics of the. Anyway, I expect that intersection and union rules might be definable in a coherent way. I'd expect no complement rule, since when the input is not of the right type, all bets are off and any result can be produced. About 4), I can't understand why that would be violating the intersection rule.
– chi
Sep 14, 2018 at 11:42
• I believe "the" has the same semantics as a type assertion. Sep 14, 2018 at 18:52

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.

• The reason I think it is a contradiction is the following. Let $A$, $B$, and $X$ be types such that $A\to X \neq (A\cap B)\to X$. Then, $A\to X \subset (A\cap B) \to X = (A\to X) \cap (B\to X) \subset A\to X$. Which means $A\to X = (A\cap B)\to X$ which is a contradiction. Sep 15, 2018 at 18:04
• I added an edit that hopefully clarifies where the chain of reasoning there breaks (or, how exactly the lisp documentation is wrong, if it is). I'm making this comment because I don't know if you'll get notified of the edit. Sep 16, 2018 at 1:20
• @Don, What the CL specification says is (for me) hard to reason about. As I interpret it says that if there are ever two declarations in scope $F:(A\to X)$ and simultaneously $F:(B\to Y)$, then the compiler \emph{may assume} that $F:((A\cap B)\to (X\cap Y))$. This sounds to me, as you claim, like the specification is saying $(A\to X) \cap (B\to Y) \subset (A\cap B) \to (X \cap Y)$, (or do I have it backwards?). I think you are right in that the specification was not claiming that this is the arrow type intersection equivalence formula. Sep 16, 2018 at 9:05
• The specification is here: clhs.lisp.se/Body/t_fn.htm, but if someone is not intimately familiar with the specification it might be difficult to read. Sep 16, 2018 at 9:06
• @JimNewton You can get a BibTeX/amsrefs block via the cite link at the bottom of the answer. For a citation, that's probably what you should use. For something more like an acknowledgement, the full name should be sufficient, though you may want to make sure you use "Dan" and not "Don"... Sep 17, 2018 at 1:39