Why does the type signature look like this? (Converting Church number to Int)

Question

I'm learning Haskell and trying to write a function that convert a Church number into a Int. My code works only if I don't write a type signature.

type Church a = (a -> a) -> a -> a

zero :: Church a
zero s z = z

c2i :: Church a -> Int   -- This line fails
c2i x = x (+1) 0

I've got the right type signature of c2i using :t c2i

c2i :: (Num a1, Num a) => ((a -> a) -> a1 -> t) -> t

but I'm wondering why it is?

chi chi · Accepted Answer · 2015-01-27T10:17:49

If you use a in the c2i signature, then it has to work with any a. In other words, a is chosen by the caller of your function. Concretely, it has to work with

c2i :: Church String -> Int
-- that is
c2i :: ((String -> String) -> String -> String) -> Int

Since the code does not work when a = String, the polymorphic type is invalid.

If you do not add a type, the compiler is able to infer some type making the code work. A simpler type could be:

c2i :: Church Int -> Int

or, after enabling a few extensions,

c2i :: (forall a. Church a) -> Int

In the latter case, we are specifying that a is chosen by c2i, not by the caller. The caller instead has to pass an argument which must have a polymorphic type: i.e., it has to pass a Church a for all a, not just a Church String.

Alternatively, one can even declare

type Church = forall a . (a->a)->a->a

and pass around polymorphic values, only.

Why does the type signature look like this? (Converting Church number to Int)

1 Answers