What is the fixed point of fix?

Question

A recent poster best left anonymous attempted to implement the factorial function like this:

f :: Int -> Int
f = fix f

This obviously didn't work out too well. But then I got to wondering: can I make it pass the type checker? What will its type reveal?

Answer 1

Indeed, it will type check given a more general type, thanks to polymorphic recursion:

f :: a
f = fix f

By parametricity, we can immediately see that it must be bottom, and based on the definition of fix, it must be an infinite loop rather than an exception.

chi comments, "For the same reason f = bar f will 'work' with any bar :: F a -> a where F a is any type (which may depend on a)". The definition looks like this:

foo :: forall f a .
       (forall b . f b -> b) -> a
foo g = g (foo g)

Again, the type signature is bogus by parametricity, since I can choose, for example, f ~ Const Void, at which point it is clear that the first argument is useless for producing the result.