Is it possible to implement addition on typed Church numerals using iterated incrementation?

Question

I can't find a way to define addition as repeated incrementation, despite this being possible in an untyped language. Here is my code:

{-# LANGUAGE RankNTypes #-}
type Church = forall a . (a -> a) -> (a -> a)

zero :: Church
zero = \f -> id

inc :: Church -> Church
inc n = \f -> f . n f

-- This version of addition works
add1 :: Church -> Church -> Church
add1 n m = \f -> n f . m f

-- This version gives me a compilation error
add2 :: Church -> Church -> Church
add2 n m = n inc m

The compilation error I get for add2 is

Couldn't match type `forall a1. (a1 -> a1) -> a1 -> a1'
                  with `(a -> a) -> a -> a'
    Expected type: ((a -> a) -> a -> a) -> (a -> a) -> a -> a
      Actual type: Church -> (a -> a) -> a -> a
    In the first argument of `n', namely `inc'
    In the expression: n inc m
    In an equation for `add2': add2 n m = n inc m

Why is this an error? Isn't Church a synonym for that ((a->a) -> a -> a) ?

Answer 1

I could not get your code to type, no matter what extra type annotations I added, although it's possible I was not clever enough. (I also tried adding ImpredicativeTypes.) I think the problem here is that in the definition

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

a can only be instantiated with a rank-0 type (i.e. without foralls inside), which Church itself isn't. So you cannot apply a Church numeral defined this way to your inc.

However, there is a relatively simple workaround that is slightly verbose but makes everything work nicely otherwise: make Church into a newtype instead of a type, so that it can be treated as monomorphic from the outside. The following all works:

{-# LANGUAGE RankNTypes #-}
newtype Church = Church { runChurch :: forall a . (a -> a) -> (a -> a) }

zero :: Church
zero = Church (\f -> id)

inc :: Church -> Church
inc n = Church (\f -> f . runChurch n f)

add2 :: Church -> Church -> Church
add2 n = runChurch n inc