Type of functions that can pass themselves as parameters

Question

Think about the types in this computation deep, really deep

id id

From right to left, the first id has type

 a -> a

that means the second id which takes the first as argument must have type

(a -> a) -> (a -> a)

The types don't match! OK by you could say the first id actually had this later type, however this would make the second id be of type

((a -> a) -> (a -> a)) -> ((a -> a) -> (a -> a))

I thought that inspite of the fact that functions could have generic or variable types, functions where bound to some upon a computation. As I see it, it seems that a new id function is defined on every call.

Answer 1

You're correct. id is polymorphic. Each use gets its type instantiated independently. Consider something dumb like id "Hello" ++ show (id 5), for instance. In the first use, it's id :: String -> String. In the second use, it's id :: Integer -> Integer (at least with the normal defaulting rules for polymorphic literals). What you're doing by nesting calls to id is the same thing - just with some type variables thrown in, in place of concrete types, at the innermost level.

This doesn't mean the implementation changes, though. id is always the same function. The only thing that changes per use is how the type checker treats it.

By the way, this is something that can be used to crash GHC's type checker. You've already noted that the size of the type of id grows exponentially when you apply it to itself a few times. Do it a few more times, and it'll need more memory than your system has to represent the type of the outermost id.