Haskell types for functions

Question

I don't understand the answer to this question:

Q: Can Haskell find a type for the function selfapply defined by: selfapply f = f f

A: The function selfapply is not typeable in the simple system of types: we need to associate to f two types which are not compatible: α → α and α.

So I know a -> a means alpha input and alpha return, but why is it a->a and a instead of a->a->a?

Also another question regarding this topic:

Find a polymorphic type for the functions quad, double

quad x = y*y where y = x*x 
double x = x*2

How can we determine a polymorphic type for these two functions?

Answer 1

Hm, well for the first one this is because let's say f f was well typed. We're applying f so it has to be a function. Functions have the type f : A -> B for some A and B. Since f is also the argument, it must also be the case that f : A. This means that A = A -> B. Moreover since f = f f, the the type of f f is also the type of f. Since f f : B this means f : B. This means that A = B and so f : A -> A and A -> A = A as required.

For the second, what's the type of *? This is the key to understanding the type of these functions since we're applying * to the input. In Haskell * :: Num a => a -> a -> a, which must mean that our functions have the type Num a -> a -> B for some B. I'll let you figure it out from there :)

Answer 2

There are a couple of levels to your first question. As an aside, though, I recommend learning about unification if you are not already familiar with it as it is a key part of understanding type checking and type inference.

To type check selfApply provisionally give f the type a which we will solve for. (At this point it is just a unification variable, the key difference between Hindley-Milner type checking and type checking for simple types is that we'll generalize (quantify over) any unbound variables at the end.) Since we are using f as a function we know a = b -> c for new variables b and c. Since we are applying f to something of type a, namely f itself, we know b = a. There is no constraint on c, so you are correct to be confused about the provided answer since f isn't required to be a and a -> a and it could indeed be a and a -> a -> a or a and a -> Bool as well. Of course, as you no doubt understand, the issue is solving the equation a = a -> c. In attempting to unify these with traditional unification we will fail what is known as the occurs check. This check is to avoid infinite terms. Rational tree unification is, however, one way to deal with this issue and leads to equi-recursive types. Haskell intentionally does not support equi-recursive types, but O'Caml, for example, does with the -rectypes flag. To validate that c is free we can use an iso-recursive type, namely:

data X c = X (X c -> c)
selfApply f = f (X f)

which will type check, and, in particular, selfApply :: (X c -> c) -> c.

There are two reasons Haskell (and almost all polymorphic languages) do not support equi-recursive types. First, pragmatically, many type errors show up as infinite types and if equi-recursive types were supported (tacitly) then they'd turn into broken but type correct programs. More philosophically, outlawing equi-recursive types and similar things was exactly why type systems were originally invented going all the way back to Bertrand Russell.