I would like to define the following function:

f a = f

This function takes one argument and returns itself ignoring the argument. Just writing it like this in ghci gives me the following type error:

• Couldn't match expected type ‘t’ with actual type ‘p0 -> t’
   ‘t’ is a rigid type variable bound by
    the inferred type of f :: t

If the function would use this argument it would be possible (as in this halt example):

halt = halt

or with one parameter

halt x = halt x

Would it somehow be possible to name this type or compile the former program? Of course, this is not for any specific reason, just trying to understand type theory, specifically in haskell, better - you could never apply this function enough to yield a specific result.

CodePudding user response：

Well, you can "almost" have that.

As already mentioned, you can't have an infinite type like a -> b -> c -> ..., since Haskell types must be finite.

However, we can define a recursive newtype which is "morally" the infinite type above, and use that:

newtype F = F { unF :: forall a. a -> F }

f :: F
f = F (\x -> f)

In simpler terms, this constructs a type F satisfying F ~= forall a . a -> F which is the equation giving rise to the wanted "infinite" type.

Note the use of the forall a to allow x to have any type at all. The (almost-)function f is essentially a "hungry" function that will eat any argument, of any type, and return itself.

There is a downside, though, to this approach. To actually apply f, we need to unwrap the constructor. This leads to code like

g :: F
g = unF (unF f True) "hello"

which is a bit more inconvenient than g = f True "hello".