In the paper Practical type inference for arbitrary-rank types, the covariance and contravariance rules are essential when dealing with function types. Covariance applies to the return types of functions, while contravariance applies to the argument types.
In (∀b. [b] → [b]) → Bool < (∀a. a → a) → Bool, the types are compared in a contravariant manner for the input types, which means the more general type must be on the right side. Here, the type a → a is more general than [b] → [b], making the inequality hold. However, in the case of [b] → Int < a → Int, the argument types are compared contravariantly. For contravariance to hold, the left-hand side argument must be more specific than the right-hand side. Since a can be any type and [b] is a specific type (a list of b), the inequality holds but it should not, for example you can not type annotate length function with a -> Int.
In my opinion, the correct relationship would be a → Int < [b] → Int, and this happens by matching a with [b].
I've been reading some papers on type inference, particularly around co- and contravariant rules for functions. I understand where the contravariant rule comes from, but I don't understand why it doesn't work for examples like [b] → Int < a → Int.
Could someone explain why the contravariant rule doesn't apply here, or if I'm misunderstanding something fundamental?
If you ask me for a way to rearrange lists (∀b. [b] → [b]), I can give you the identity function (∀a. a → a), because it’s the simplest rearranger of lists.
example1 :: forall b. [b] -> [b]
example1 = id @[b]
If you want a predicate about identity functions ((∀a. a → a) → Bool)—which is really no better than a constant Boolean—then I can get away with giving you a predicate about list-rearrangers ((∀b. [b] → [b]) → Bool), because I know you’ll only ever call it on the identity function.
example2 :: (forall a. a -> a) -> Bool
example2 = reverses
reverses :: (forall b. [b] -> [b]) -> Bool
reverses f = f @Int [1, 2, 3] == [3, 2, 1]
If you want a function that computes an integer from a single list of values of any type (∀b. [b] → Int), I can give you a function that doesn’t use its argument, and just returns a constant integer (∀a. a → Int).
example3 :: forall b. [b] -> Int
example3 = const @[b] @Int 789
If you ask for a constant function, I can’t give you length, because it does examine its argument.
nonexample4 :: forall a. a -> Int
nonexample4 = length -- error
But if what you’re asking for is a function that computes an integer from a source of lists of any element type ((∀b. [b]) → Int), the only thing those lists can be is the empty list [], so unlike length, this is as good as a constant integer function.
example5 :: (forall b. [b]) -> Int
example5 xs = 456
where
noInts = xs @Int
noChars = xs @Char
noVoids = xs @Void
example4 :: forall a. a -> Int
example4 = example5
Moreover, if you ask for a function that makes an integer from a magical wellspring of anything I want ((∀a. a) → Int), then I can play make-believe all I want, but I know that well is dry—you’ll never actually call it with anything but bottom.
example6 :: (forall a. a) -> Int
example6 magic = anyInt + ord anyChar
where
anyInt = magic @Int
anyChar = magic @Char
anyVoid = magic @Void -- oh no
So in the end the variance depends not only on function arrows, but also quantifiers: