What Justification for the type of f x = f x in Haskell is there?

Haskell gives f x = f x the type of t1 -> t, but could someone explain why?

And, is it possible for any ot开发者_如何学编程her, nonequivalent function to have this same type?

Okay, starting from the function definition f x = f x, let's step through and see what we can deduce about the type of f.

Start with a completely unspecified type variable, a. Can we deduce more than that? Yes, we observe that f is a function taking one argument, so we can change a into a function between two unknown type variables, which we'll call b -> c. Whatever type b stands for is the type of the argument x, and whatever type c stands for must be the type of the right-hand side of the definition.

What can we figure out about the right-hand side? Well, we have f, which is a recursive reference to the function we're defining, so its type is still b -> c, where both type variables are the same as for the definition of f. We also have x, which is a variable bound within the definition of f and has type b. Applying f to x type checks, because they're sharing the same unknown type b, and the result is c.

At this point everything fits together and with no other restrictions, we can make the type variables "official", resulting in a final type of b -> c where both variables are the usual, implicitly universally quantified type variables in Haskell.

In other words, f is a function that takes an argument of any type and returns a value of any type. How can it return any possible type? It can't, and we can observe that evaluating it produces only an infinite recursion.

For the same reason, any function with the same type will be "equivalent" in the sense of never returning when evaluated.

An even more direct version is to remove the argument entirely:

foo :: a
foo = foo

...which is also universally quantified and represents a value of any type. This is pretty much equivalent to undefined.

f x = undefined

has the (alpha) equivalent type f :: t -> a.

If you're curious, Haskell's type system is derived from Hindley–Milner. Informally, the typechecker starts off with the most permissive types for everything, and unifies the various constraints until what remains is consistent (or not). In this case, the most general type is f :: t1 -> t, and there's no additional constraints.

Compare to

f x = f (f x)

which has inferred type f :: t -> t, due to unifying the types of the argument of f on the LHS and the argument to the outer f on the RHS.