Haskell中教会编码的布尔的xor

Question

我目前正在尝试为xor实现lambda表达式.但是,我觉得我错过了一些东西,因为我从bxor表达式中得到了错误.我究竟做错了什么？

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

Answer 1

在打字环境中,需要小心.你的lambda术语在无类型设置中工作正常,但需要在键入的一个中进行一些调整.

我们需要为教会布尔定义一种类型.让我们选择以下参数单态类型.

type B a = a -> a -> a

然后,让我们添加类型注释来检查错误:

true :: B a
true  = \t f -> t

false :: B a
false = \t f -> f

toBool :: B Bool -> Bool
toBool = \b -> b True False

到现在为止还挺好.然而:

bnot :: B a -> B a
bnot = \b -> b false true

产生类型错误,因为例如false有类型B a,而不是a,因此应用程序b false是错误的类型.我们可以通过添加几个a参数来解决这个问题x y,并相应地简化函数.

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

这种类型检查.同样,我们可以重做bxor以进行类型检查:

bxor :: B a -> B a -> B a       
bxor = \b1 b2 x y -> b1 (bnot b2 x y) (b2 x y)

或者,使用布尔值的impredicative Church编码,除了添加相关类型签名外,我们可以使原始代码按原样进行类型检查.这需要更高级别的类型.

{-# 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