Confused about function subtyping

Question

I'm taking a course on programming languages and the answer to "when is a function a sub type of another function" is very counter-intuitive to me.

To clarify: suppose that we have the following type relation:

bool<int<real

Why is the function (real->bool) a subtype of (int->bool)? Shouldn't it be the other way around?

I would expect the criteria for sub typing functions to be: f1 is a subtype of f2 if f2 can take any argument that f1 can take, and f1 returns only values that f2 returns. There clearly are values that f1 can take, but f2 can't.

Answer 1

Here's the rule for function sub-typing:

Argument types must be co-variant, return types must be contra-variant.

Co-variant == preserves the "A is a subtype of B" hierarchy for the type of the results parameter. Contra-variant == reverses ("goes against") the type hierarchy for the arguments parameter.

So, in your example:

f1:  int  -> bool
f2:  bool -> bool

We can safely conclude that f2 is a subtype of f1. Why? Because (1) looking at just the argument types for both functions, we see that the type hierarchy of "bool is a subtype of int" is in fact co-variant. It preserves the type hierarchy between ints and bools. (2) looking at just the results types for both functions, we see that contra-variance is upheld.

Put another way (the plain English way I think about this subject):

co-variant arguments: "my caller can pass in more than I require, but that's okay, because I'll use only what I need to use." contra-variant arguments: "I can return more than the caller requires, but that's okay, he/she will just use what they need, and will ignore the rest"

Let's look at another examples, using structs where everything is an integer:

f1:  {x,y,z} -> {x,y}
f2:  {x,y}   -> {x,y,z}

So here again, we're asserting that f2 is a subtype of f1 (which it is). Looking at the argument types for both functions (and using the < symbol to denote "is a subtype of"), then if f2 < f1, is {x,y,z} < {x,y} ? The answer is yes. {x,y,z} is co-variant with {x,y}. i.e. in defining the struct {x,y,z} we "inherited" from the {x,y} struct, but added a third member, z.

Looking at the return types for both functions, if f2 < f1, then is {x,y} > {x,y,z}? The answer again is yes. (See above logic).

Yet a third way to think about this, is to assume f2 < f1, then try various casting scenarios, and see if everything works. Example (psuedo-code):

   F1 = f1;
   F2 = f2;
   {a,b}   = F1({1,2,3});  // call F1 with a {x,y,z} struct of {1,2,3};  This works.
   {a,b,c} = F2({1,2});    // call F2 with a {x,y} struct of {1,2}.  This also works.

   // Now take F2, but treat it like an F1.  (Which we should be able to do, 
   // right?  Because F2 is a subtype of F1).  Now pass it in the argument type 
   // F1 expects.  Does our assignment still work?  It does.
   {a,b} = ((F1) F2)({1,2,3});