Unification of higher rank types on contravariant positions

Question

Quick example:

{-# LANGUAGE RankNTypes #-}                                

l :: (forall b. [b] -> [b]) -> Int                         
l f = 3                                                    

l1 :: forall a. a -> a                                     
l1 x = x                                                   

l2 :: [Int] -> [Int]                                       
l2 x = x                                                   


k :: ((forall b. [b] -> [b]) -> Int) -> Int                
k f = 3                                                    

k1 :: (forall a. a -> a) -> Int                            
k1 x = 99                                                  

k2 :: ([Int] -> [Int]) -> Int                              
k2 x = 1000 


m :: (((forall b. [b] -> [b]) -> Int) -> Int) -> Int                                           
m f = 3                                                                                        

m1 :: ((forall a. a -> a) -> Int) -> Int                                                       
m1 x = 99                                                                                      

m2 :: (([Int] -> [Int]) -> Int) -> Int                                                         
m2 x = 1000

Here:

l l1 typechecks
l l2 does not typecheck
k k1 does not typecheck
k k2 typechecks
m m1 typechecks
m m2 does not typecheck

While I am totally okay with what happens in l and m I don't understand the k part. There is some kind of relation of being "more polymorphic", for instance forall a. a -> a is more polymoprhic than forall b. [b] -> [b] because one can just substitute a/[b]. But why does this relation flip if the polymorphic types are on contravariant positions?

As I see k expects "a machine that takes machine operating on any lists that produces Int". k1 is "a machine that takes any endomorphism-machine that produces int". k1 offers therefore much more than k wants, so why doesn't it fit its requirements? I feel there is some mistake in my reasoning, but I can't get it...

chi chi · Accepted Answer · 2020-03-05T00:18:05

The type of k promises that, when called as k f, each call to f will have as an argument a function of type (forall b. [b] -> [b]).

If we choose f = k1, we pass something that wants as input a function of type forall a. a->a. This won't be satisfied when k calls f = k1 with a less general function (of type (forall b. [b] -> [b])).

More concretely, consider this:

k :: ((forall b. [b] -> [b]) -> Int) -> Int 
k f = f (\xs -> xs++xs)

k1 :: (forall a. a -> a) -> Int                            
k1 x = x 10 + length (x "aaa")

Both type check. However, reducing k k1 we get:

k k1 =
k1 (\xs -> xs++xs) =
(\xs -> xs++xs) 10 + length ((\xs -> xs++xs) "aaa") =
(10++10) + length ("aaa"++"aaa")

which is ill-typed, so k k1 must be ill-typed as well.

Therefore, yes -- contravariant positions do reverse the order of subtyping (aka "being less general"). For A -> B to be more general than A' -> B', we want the former to put fewer requirements on the input (A must be less general than A') and to provide more guarantees on the output (B must be more general than B').

Unification of higher rank types on contravariant positions

1 Answers