I'm playing with Rank-N-type and trying to type x x. But I find it counter intuitive that these two functions can be typed in the same way.

f :: (forall a b. a -> b) -> c
f x = x x

g :: (forall a b. a -> b) -> c
g x = x x x x x

I have also noticed that something like f x = x x ... x x (many xs) still has the same type. Can anyone explain why it is the case?

CodePudding user response：

The key is that x :: a -> b is a function that can provide a value of any type, no matter what argument is given. That means x can be applied to itself, and the result can be applied to x again, and so on and so on.

At least, that's what it promises the type checker it can do. The type checker isn't concerned about whether or not any such value exists, only that the types align. Neither f nor g can actually be called, because no such value of type a -> b exists (ignoring bottom and unsafeCoerce).

CodePudding user response：

This shouldn't really be any more surprising than the fact that

m :: (∀ a . a) -> (∀ a . a) -> (Int, Bool)
m p q = (p, q)

has the same type as

n :: (∀ a . a) -> (∀ a . a) -> (Int, Bool)
n p q = (q, p)

Much like in your example, this works because the universally-quantified argument can be used in lots of different way, with the compiler in each case choosing an appropriate type and enforcing x to act as having that type.

This is actually a rather contrived situation because types like ∀ a . a or ∀ a b . a->b are uninhabited (modulo ⊥), so you would never actually be able to use a RankN function with such an argument; pragmatically you wouldn't even write it either then!

Practically useful RankN functions usually impose some extra structure or typeclass constraint in their arguments, like

foo :: (∀ a . [a] -> [a]) -> ...

qua :: (∀ n . Num n -> Int -> n -> n) -> ...

CodePudding user response：

A simpler example

This is a phenomenon that can be observed whenever we use a variable which has a polymorphic type (like your x). The identity function id is perhaps the most famous example.

id :: forall a . a -> a

Here, all these expressions type check, and have type Int -> Int:

id :: Int -> Int
id id :: Int -> Int
id id id :: Int -> Int
id id id id :: Int -> Int
...

How is that possible? Well, the crux is that each time we write id we are actually meaning "the identity function on some unknown type a that should be inferred from the context". Crucially, each use of id has its own a.

Let's write id @T to mean the specific identity function on type T.

Writing

id :: Int -> Int

actually means

id @Int :: Int -> Int

which is straightforward. Instead, writing

id id :: Int -> Int

actually means

id @(Int -> Int) (id @Int) :: Int -> Int

where the first id now refers to the function space Int -> Int! And, of course,

id id id :: Int -> Int

means

(id @((Int -> Int) -> (Int -> Int))) (id @(Int -> Int)) (id @Int) :: Int -> Int

And so on. We do not realize that types get that messy since Haskell infers those for us.

The specific case

In your specific case,

g :: (forall a b. a -> b) -> c
g x = x x x x x

we can make that type check in many ways. A possible way is to define A ~ Int, B ~ Bool, T ~ (A -> B) and then infer:

g x = x @T @(T -> T -> T -> c) (x @A @B) (x @A @B) (x @A @B) (x @A @B)

I suggest to spend some time to realize that everything type checks. (Moreover our choices of A and B are completely arbitrary, and we could use any other types there. We could even use distinct As and Bs for each x, as long as the first x is suitably instantiated!)

It is then obvious that such inference is also possible even when x x x ... is a longer sequence.