Haskell fixed point signature

Question

What is the signature of the following Haskell function:

fix f = f (fix f)

a) ((a->b)->a->b)->a->b

b) The signature can not be synthesized

c) (a->a)->a

Thanks!

Answer 1

This question looks like an course homework / test question. I'll help you to find the solution yourself:

First you probably have GHC installed, so you can run ghci a haskell repl.

There is a section in GHC users' guide about GHCi. Yet it's quite long.

If you start up the GHCi you'll get a prompt, where you can type Haskell expressions:

Prelude> 1 + 1
2
Prelude> map (\x -> x + x) [1, 2, 3]
[2,4,6]

You can also bind expression to names, and define functions:

Prelude> let fix f = f (fix f)

And one of the most powerful features is to ask for the type of the expression:

Prelude> :t map (\x -> x + x)
map (\x -> x + x) :: Num b => [b] -> [b]
Prelude> :t fix
... output omitted

That's how you find a solution to your problem. After you know that, you could ask why the type of fix is what it is.

Answer 2

A completely different approach: finding the solution through reasoning.

The right hand side is

f (fix f)

so f has the type a -> b for some types a and b, since f is a function.

In other words, the value of f (fix f) has type b, and fix f has the type a.

Since, by definition,

fix f = f (fix f)

fix f must have the same type as f (fix f), i.e. b.

We have already said that a is the type of fix f, so a and b must be the same type.

Let's call it t to keep things separate.

So f : t -> t, since a and b were the same type t.
We know that fix f has the type b, which we renamed t.

Putting f : t -> t and fix f : t together we get

fix : (t -> t) -> t  

which is alternative c).

---

Aside: if we substitute a -> b for t we get

((a -> b) -> (a -> b)) -> (a -> b)

or, since the arrow associates to the right:

((a -> b) -> a -> b) -> a -> b

which is exactly the answer in a).
So a) is almost correct, but not general enough.