Hindley-Milner type of a function that takes itself as an argument

Question

Suppose you had a function f that would be used as follows:

(f f (x-1)) 

What can you deduce about the type of f?

It seems to be recursive, ie, f :: (ftype) -> int -> int.

Answer 1

If an argument to a function is that function itself, then the type would have to be recursive and infinite in a way that's illegal in Haskell. There's one loophole, however: if the function is polymorphic in that argument, then it's fine (although probably not very useful as a function). Two examples of a valid f are id and const id (with either of them, f f (x-1) would just evaluate to x-1).

Answer 2

In your title, you ask about the "Hindley-Milner type" of f. In usual parlance, the HM type of an expression is the principal (most general) type inferred for the expression through the formal HM type inference rules applied to a particular context. So, f has no type without a context, and the expression f f (x-1) doesn't provide enough information about the context to type f. Contexts can be given "at the start" or can develop through the use of lambda or let expressions. The context that develops will determine if an HM type can be inferred for f and, if so, what that type is.

For example, the larger expression:

let f = \y -> y in \x -> f f (x-1)

can be typed in the empty context. Without going through the details, it infers the type forall a. a -> a for f and the type Integer -> Integer for the whole expression, provided the - operator is Integer subtraction. (The HM type system doesn't have a concept of type classes and constraints, like Num.) So, here, the HM type for f is forall a. a -> a, and its use in the expression f f (x-1) doesn't really affect its type. This is typical for expressions where f is introduced with a let expression. For example, the larger expression:

let f = \y -> \z -> y in \x -> f f (x-1)

is also well typed. The type inferred for f is forall a b. a -> b -> a (which is the obvious type for \y -> \z -> y and is not influenced by the rest of the expression). The overall expression has type forall a b. Integer -> a -> b -> a.

In contrast, if f is introduced through a lambda expression, then things are different, and the expression f f (x-1) does influence the inferred type for f. For example, the larger expression:

\f -> \x -> f f (x-1)

is ill-typed in HM and so doesn't infer a type for f or for the expression as a whole. If the body of the double-lambda is changed, then different HM types can be inferred for f depending on the expression:

\f -> \x -> f (f x x) (x-1)   -- f :: Integer -> Integer -> Integer
\f -> \x -> f x + f x         -- f :: forall a. a -> Integer

Sooooo... to sum up, no type is inferred for f from the expression f f (x-1) alone because the context is insufficient. In a context where f is introduced by a let expression, the type of f will be inferred strictly from the definition of f, and as long as the type is compatible with the expression f f (x-1), type inference will succeed. Conversely, in a context where f is introduced by a lambda expression, the expression f f (x-1) is ill-typed, so no type for f can be inferred.

Answer 3

To answer the question you could apply a type-inference algorithm. Going about it informally, you can start by stating that f :: a -> b -> c because it takes two curried arguments. You can also infer the constraint Num b because of x - 1, so f :: Num b => a -> b -> c. Possibly more if you know what type x is. But that's about it.

For example, the function could be defined as f g x = undefined, in which case both of its arguments are discarded, and the return type does not unify with any of the input types. If f had a function body then you could infer a lot more.