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?
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:
{-# LANGUAGE ImpredicativeTypes #-} to the top of your filetype ChurchNum = forall a. (a -> a) -> a -> a to your fileadd, mul, and exp functions the type signature ChurchNum -> ChurchNum -> ChurchNumI'd highly advise you to write similar types for the rest of your definitions.