Why are two polymorphic higher order functions with different type vars equivalent regarding their types?

Question

Coming from Javascript I understand that Haskell's list type enforces homogeneous lists. Now it has surprised me that the following different function types meet this requirement:

f :: (a -> a) -> a -> a 
f g x = g x

g :: (a -> b) -> a -> b 
g h x = h x

let xs = [f, g] -- type checks

even though g is more widely applicable than f:

f(\x -> [x]) "foo" -- type error
g(\x -> [x]) "foo" -- type checks

Shouldn't (a -> a) be treated diffenrently than (a -> b). It seems to me as if the latter is a subtype of the former. But there are no subtype relationships in Haskell, right? So why does this work?

Ambiguity

Haskell's type inference algorithm says "Can I come up with a substitution which makes these two types the same?" The types of f and g unify, under the substitution b ~ a, at the type (a -> a) -> a -> a. So xs :: [(a -> a) -> a -> a]. – Weaponeer

@Benjamin OK, it passes the type check because of the lack of code that Haskell's type inference can work with. For the given code the assertion that these two types may be equivalent is simply sufficient. – Ambiguity

I think Haskell isn't rigid in this example in order to minimize the number of programs that are beyond the expressiveness of its type system. i. e. programs that do not compile, but would still make sense. – Ambiguity

Answer 1

Haskell is statically typed, but that doesn't mean it's Fortran. Every type must get fixed at compile time, but not necessarily within a single definition. The types of both f and g are polymorphic. One way to interpret this is that f is not just a single function, but a whole family of overloaded functions. Like (in C++)

int f (function<int(int)> g, int x) { return g(x); }
char f (function<char(char)> g, char x) { return g(x); }
double f (function<double(double)> g, double x) { return g(x); }
...

Of course it wouldn't be practical to actually generate all of these functions, so in C++ you'd instead write this as a template

template <typename T>
T f (function<T(T)> g, T x) { return g(x); }

...meaning, whenever the compiler finds f if your project's code, it'll figure out what T is in the specific case, then create a concrete template instantiation (a monomorphic function fixed to that concrete type, like the example ones I wrote above) and only use that concrete instantiation at runtime.

These concrete instantiations of two template-functions may then have the same type, even if the templates looked a bit different.

Now, Haskell's parametric polymorphism is resolved a little bit different from C++ templates, but at least in your example they amount to the same: g is a whole family of functions, including the instantiation g :: (Int -> Char) -> Int -> Char (which is not compatible with the type of f) but also g :: (Int -> Int) -> Int -> Int, which is. When you put f and g in a single list, the compiler automatically realises that only the subfamily of g whose type is compatible with f is relevant here.

Yes, this is indeed a form of subtyping. When we say “Haskell doesn't have subtyping” we mean that any concrete (Rank-0) type is disjoint from all other Rank-0 types, but polymorphic types may overlap.

Typehigh

So when these two types are merely added to a list it is sufficient for the type checker that f's and g's polymorphic types have some ground types in common. But as soon as I map a pure function of type (a -> b) over this list, type inference will detect the type error. Haskell's type inference weighs up every single case and is only as restrictive as needed. That's brilliant again. – Ambiguity

Answer 2

@leftroundabout’s answer is solid; here’s a more technical supplementary answer.

There is a sort of subtyping relationship at work in Haskell: the System F “generic instance” relation. This is what the compiler uses when checking the inferred type of a function against its signature. Basically, the inferred type of a function must be at least as polymorphic as its signature:

f :: (a -> a) -> a -> a
f g x = g x

Here, the inferred type of f is forall a b. (a -> b) -> a -> b, the same as the definition of g you gave. But the signature is more restrictive: it adds the constraint a ~ b (a is equal to b).

Haskell checks this by first replacing the type variables in the signature with Skolem type variables—these are fresh unique type constants that only unify with themselves (or type variables). I’ll use the notation $a to represent a Skolem constant.

forall a. (a -> a) -> a -> a
($a -> $a) -> $a -> $a

You may see references to “rigid, Skolem” type variables when you accidentally have a type variable that “escapes its scope”: it’s used outside the forall quantifier that introduced it.

Next, the compiler does a subsumption check. This is essentially the same as normal unification of types, where a -> b ~ Int -> Char gives a ~ Int and b ~ Char; but because it’s a subtyping relationship, it also accounts for covariance and contravariance of function types. If (a -> b) is a subtype of (c -> d), then b must be a subtype of d (covariant), but a must be a supertype of c (contravariant).

{-1-}(a -> b) -> {-2-}(a -> b)  <:  {-3-}($a -> $a) -> {-4-}($a -> $a)

{-3-}($a -> $a) <: {-1-}(a -> b)  -- contravariant (argument)
{-2-}(a -> b) <: {-4-}($a -> $a)  -- covariant (result)

The compiler generates the following constraints:

$a <: a  -- contravariant
b <: $a  -- covariant
a <: $a  -- contravariant
$a <: b  -- covariant

And solves them by unification:

a ~ $a
b ~ $a
a ~ $a
b ~ $a

a ~ b

So the inferred type (a -> b) -> a -> b is at least as polymorphic as the signature (a -> a) -> a -> a.

---

When you write xs = [f, g], normal unification kicks in: you have the two signatures:

forall a.   (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b

These are instantiated with fresh type variables:

(a1 -> a1) -> a1 -> a1
(a2 -> b2) -> a2 -> b2

Then unified:

(a1 -> a1) -> a1 -> a1  ~  (a2 -> b2) -> a2 -> b2
a1 -> a1  ~  a2 -> b2
a1 -> a1  ~  a2 -> b2
a1 ~ a2
a1 ~ b2

And finally solved & generalised:

forall a1. (a1 -> a1) -> a1 -> a1

So the type of g has been made less general because it’s been constrained to have the same type as f. The inferred type of xs will therefore be [(a -> a) -> a -> a], so you’ll get the same type error writing [f (\x -> [x]) "foo" | f <- xs] as you did writing f (\x -> [x]) "foo"; even though g is more general, you’ve hidden away some of that generality.

---

Now you might be wondering why you would ever give a more restrictive signature for a function than necessary. The answer is—to guide type inference and produce better error messages.

For example, the type of ($) is (a -> b) -> a -> b; but in fact this is a more restrictive version of id :: c -> c! Just set c ~ a -> b. So in fact you can write foo `id` (bar `id` baz quux) instead of foo $ bar $ baz quux, but having this specialised identity function makes it clear to the compiler that you expect to use it to apply functions to arguments, so it can bail out earlier and give you a more descriptive error message if you make a mistake.

Telfer

Doesn't co/contravariance only really come into play for higher-rank types? Without RankNTypes, all the foralls are on the outside, and class constraints are always "contravariant". But maybe I'm wrong.... – Portemonnaie

@dfeuer: Yes, I think that’s the only time contravariance matters. To use an example from §3.3 of this paper, given f ∷ ((∀a. [a] → [a]) → Int) → Int, g ∷ (∀a. a → a) → Int, and h ∷ ([Int] → [Int]) → Int, ∀a. a → a is more polymorphic than ∀a. [a] → [a], and therefore (∀a. a → a) → Int is less polymophic than (∀a. [a] → [a]) → Int, which is why f g is a type error but f h is fine. – Telfer

Thank you for this insight into the machinery. I'll take a closer look at the subsumption process and the type constants. – Ambiguity

If I understand your answer correctly, type vars are replaced by fresh skolem type vars whenever an explicit user-defined type annotation is provided, in order to distinguish them from programmatically inferred type variables. And subsumption is unification that takes the "more polymorphic than" relation into account, which describes a kind of subtyping. Is this correct? – Ambiguity

@ftor: Yup, that’s correct. The first part of my answer describes why you can use a less-general type signature; the second part describes why you can put multiple functions of different (but compatible) types in a homogeneous list. – Telfer

The more I study polymorphism and unification the more I appreciate your answer. For rank-1 types covariance matters. For higher-rank polymorphism contravariance matters too. This answer definitely deserves more upvotes. – Ambiguity