Implementation of Church numeral multiplication in Haskell not working

Question

I'm currently learning about Church encoding and I'm trying to implement the mul (multiply) function. This is the correct implementation mul cn cm = \f x -> cn (cm f) x

This (my implementation) doesn't work, It gives a type error mul cn cm = cn (add cm) zero

Why is this so?

The error described for the mul cn cm = cn (add cm) zero

ghci> unchurch (mul (church 3) (church 4))

<interactive>:2:16: error:
    * Couldn't match type `t2' with `(t2 -> t2) -> t3 -> t2'
      Expected: (((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                  -> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                      -> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                  -> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                  -> ((t2 -> t2) -> t3 -> t2)
                  -> (t2 -> t2)
                  -> t3
                  -> t2)
                 -> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                 -> ((t2 -> t2) -> t3 -> t2)
                 -> (t2 -> t2)
                 -> t3
                 -> t2)
                -> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                    -> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                        -> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                    -> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                    -> ((t2 -> t2) -> t3 -> t2)
                    -> (t2 -> t2)
                    -> t3
                    -> t2)
                -> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                -> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                    -> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                -> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                -> ((t2 -> t2) -> t3 -> t2)
                -> (t2 -> t2)
                -> t3
                -> t2
        Actual: (((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                  -> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                      -> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                  -> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                  -> ((t2 -> t2) -> t3 -> t2)
                  -> (t2 -> t2)
                  -> t3
                  -> t2)
                 -> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                 -> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                     -> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                 -> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                 -> ((t2 -> t2) -> t3 -> t2)
                 -> (t2 -> t2)
                 -> t3
                 -> t2)
                -> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                    -> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                        -> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                    -> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                    -> ((t2 -> t2) -> t3 -> t2)
                    -> (t2 -> t2)
                    -> t3
                    -> t2)
                -> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                -> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                    -> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                -> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                -> ((t2 -> t2) -> t3 -> t2)
                -> (t2 -> t2)
                -> t3
                -> t2
      `t2' is a rigid type variable bound by
        the inferred type of
          it :: (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
                -> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2
        at <interactive>:2:1-36
    * In the first argument of `mul', namely `(church 3)'
      In the first argument of `unchurch', namely
        `(mul (church 3) (church 4))'
      In the expression: unchurch (mul (church 3) (church 4))
    * Relevant bindings include
        it :: (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
              -> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2
          (bound at <interactive>:2:1)

Full Code

module Church where

import Prelude hiding (not, and, or, fst, snd, add, iszero, zero, one, two, three, mul, exp)

-- | Church Booleans
--
-- You will see that the above macros for true, false and iff are behaving as expected. 
-- For example, one may verify that iff true M N is equivalent to M, and iff false M N is equivalent to N.
--
-- >>> iff true "M" "N"
-- "M"
--
-- >>> iff false "M" "N"
-- "N"
--
-- Boolean arithmetic is also encodable in this way. For example, 
-- Boolean negation is essentially flipping the two “branches’ ’:
-- 
-- >>> iff (not true) "M" "N"
-- "N"


true t f = t
false =  \t f -> f
iff   =  \b t f -> b t f

not b =  \t f -> b f t


-- | Church Booleans - Test
--
-- >>> iff (and true false) "get true" "get false"
-- "get false"
--
-- >>> iff (and true true) "get true" "get false"
-- "get true"
--
-- >>> iff (and false true) "get true" "get false"
-- "get false"
--
-- >>> iff (and false false) "get true" "get false"
-- "get false"
--
-- >>> iff (or true false) "get true" "get false"
-- "get true"
--
-- >>> iff (or true true) "get true" "get false"
-- "get true"
--
-- >>> iff (or false true) "get true" "get false"
-- "get true"
--
-- >>> iff (or false false) "get true" "get false"
-- "get false"
--
-- >>> iff (not (or true false)) "get true" "get false"
-- "get false"


and b1 b2 = \t f -> if (b1 t f, b2 t f) == (t, t) then t else f
or  b1 b2 = \t f -> if (b1 t f, b2 t f) == (f, f) then f else t

-- |- Church Pairs
--
-- For pairs, we need three operations mkpair, fst, and snd that obey the following behavior:
-- 
-- >>> fst (mkpair "M" "N")
-- "M"
--
-- >>> snd (mkpair "M" "N")
-- "N"

mkpair x y   = \s -> iff s x y
fst p        = p true
snd p        = p false


-- |- Church Triples
-- 
-- >>> fst3 (mktriple "M" "N" "P")
-- "M"
--
-- >>> snd3 (mktriple "M" "N" "P")
-- "N"
--
-- >>> thd3 (mktriple "M" "N" "P")
-- "P"

mktriple x y z = \ b1 b2 -> iff b1 (b2 y z) x
fst3 p         = p false true
snd3 p         = p true true
thd3 p         = p true false

-- | Church Numbers
--
-- >>> unchurch (add1 zero)
-- 1
--
-- >>> unchurch (add (church 23) (church 17))
-- 40
--
-- >>> iff (iszero (church 0)) "zero is zero" "zero is not zero"
-- "zero is zero"


church 0 = \f x -> x
church n = \f x -> f (church (n-1) f x)

unchurch cn = cn (+ 1) 0

zero   = \f x -> x
one    = \f x -> f x
two    = \f x -> f (f x)
three  = \f x -> f (f (f x))


add1 cn    = \f x -> f (cn f x)

add cn cm  = cm add1 cn

iszero cn  = cn (\x -> false) true




-- | Church Numbers - Multiplications and Exponentiations
--
-- >>> unchurch (mul (church 3) (church 4))
-- 12
--
-- >>> unchurch (exp (church 2) (church 3))
-- 8

-- Dk why this doesn't work!!!!!!!!
--mul cn cm = cn (add cm) zero


mul cn cm = \f x -> cn (cm f) x
exp cn cm = cm (mul cn) one

I also found that the code below works test cn = cn (add1) zero

However this one doesn't work. This one doesn't work when I try to put in two or three but works with zero and one for some reason test2 cn = cn (add one) zero

This goes against my understanding of how currying works in haskell. Shouldn't 'add1' and 'add one' be the same?

Answer 1

The types you're using are too complicated for Haskell to infer, and also require GHC 9.2 or newer and a GHC extension. Assuming you're on a new enough GHC version, the minimal changes to your program for your mul definition to work are as follows:

1. Add {-# LANGUAGE ImpredicativeTypes #-} to the top of your file
2. Add type ChurchNum = forall a. (a -> a) -> a -> a to your file
3. Give the add, mul, and exp functions the type signature ChurchNum -> ChurchNum -> ChurchNum

I'd highly advise you to write similar types for the rest of your definitions.