I'm currently trying to implement a lambda expression for xor. However, I feel like I'm missing something because I am getting errors from by bxor expression. What am I doing wrong?
true = \t f -> t -- always pick the first argument
false = \t f -> f -- always pick the second argument
toBool = \b -> b True False
bnot = \b -> b true false
bxor = \b x -> b (bnot x) x
In a typed environment, one needs to be careful. Your lambda-terms work fine in an untyped setting, but need some tweaks in a typed one.
We need to define a type for Church booleans. Let's choose the following parametric monomorphic type.
type B a = a -> a -> a
Then, let's add type annotations to check what's wrong:
true :: B a
true = \t f -> t
false :: B a
false = \t f -> f
toBool :: B Bool -> Bool
toBool = \b -> b True False
So far, so good. However:
bnot :: B a -> B a
bnot = \b -> b false true
yields a type error, since e.g. false has type B a, not a, so the application b false is ill-typed. We can work around this by adding a couple of a arguments x y, and simplifying the function accordingly.
bnot = \b x y -> b (false x y) (true x y)
-- or, more simply:
bnot = \b x y -> b y x
-- or even
bnot = flip
This type checks. Similarly, we can rework bxor to make it type check:
bxor :: B a -> B a -> B a
bxor = \b1 b2 x y -> b1 (bnot b2 x y) (b2 x y)
Alternatively, using the impredicative Church encoding of booleans, we can make your original code to type check as it is, except for adding the relevant type signatures. This requires higher-rank types.
{-# LANGUAGE Rank2Types #-}
type BI = forall a. a -> a -> a
trueI :: BI
trueI = true
falseI :: BI
falseI = false
toBoolI :: BI -> Bool
toBoolI = \b -> b True False
bnotI :: BI -> BI
bnotI = \b -> b falseI trueI
bxorI :: BI -> BI -> BI
bxorI = \b x -> b (bnotI x) x