4

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.

Cristian Garcia
  • 9,630
  • 6
  • 54
  • 75
  • 1
    If we say `id :: a -> a`, we actually mean `id :: forall a. a -> a` ([implicit quantification](http://www.haskell.org/ghc/docs/6.12.1/html/users_guide/other-type-extensions.html)). The `a`'s in `(id :: forall a. a -> a) (id :: forall a. a -> a)` don't all refer to the same type. –  Jul 05 '14 at 16:57
  • If you think that's fun, you should try putting a bunch of `fmap`s together in ghci. E.g. : `:t fmap fmap fmap fmap fmap` returns `:: Functor f => (a1 -> b) -> (a -> a1) -> f a -> f b` – rampion Jul 05 '14 at 17:30

2 Answers2

8

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.

Carl
  • 26,500
  • 4
  • 65
  • 86
  • [Relevant](http://stackoverflow.com/q/23746852/839246) post from May about how you can crash the compiler using nested calls to `id`. – bheklilr Jul 06 '14 at 01:50
3

The correct technology to handle the situation is polymorphism. The identity function

id x = x

has type ∀α . α → α, which is read as "for every type α, id maps elements of type α to elements of type α". To give a type to the application

id id

we argue as follows:

  • the first id has type ∀α . α → α,
  • the second id has type ∀β . β → β where we renamed the bound variable α to β in order to avoid confusion,
  • if we set α in the first id to ∀β . β → β then we see that the first id maps elements of type ∀β . β → β to elements of type ∀β . β → β,
  • therefore the whole expression is ok and has type ∀β . β → β, which is the same as ∀α . α → α.

There is no mystery. Further reading: System F.

Andrej Bauer
  • 2,458
  • 17
  • 26
  • 1
    This question arose because I heard the statement for a person who studies math that said: "A function that can pass itself as a parameter has no type". If you think about static types, it might be true that you can't define the type of the function because of this recursive situation, but polymorphism breaks this. Any thoughts on the topic? – Cristian Garcia Jul 05 '14 at 19:28
  • 2
    @CristianGarcia This isn't mystifying at all; `id :: Int -> Int` and `id :: (Int -> Int) -> (Int -> Int)` are, in fact, different functions. They just happen to have the same name. There's not _the_ `id` function in mathematics, rather there's _an_ `id` function for every set (or in Haskell, every type). – Cubic Jul 05 '14 at 20:16
  • 2
    Mathematicians are not used to phenomena arising in programming languages. You can tell your mathematician friend there is a (non-trivial) topological space $D$ which is homeomorphic to its own function space of continuous maps $\mathcal{C}(D,D)$. Thus (up to isomorphism) in this space a function can be self-applied. – Andrej Bauer Jul 06 '14 at 12:30