xor von Church-encoded booleans in Haskell

Question

Ich versuche gerade, einen Lambda-Ausdruck für Xor zu implementieren. Ich fühle jedoch, dass ich etwas vermisse, weil ich durch bxor Ausdruck Fehler erhalte. Was mache ich falsch?

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

In einer typisierten Umgebung muss man vorsichtig sein. Ihre Lambda-Terme funktionieren in einer untypisierten Einstellung gut, benötigen aber einige Verbesserungen in einer getippten Einstellung.

Wir müssen einen Typ für Church Booleans definieren. Wählen wir den folgenden parametrischen monomorphen Typ.

type B a = a -> a -> a 

Dann lassen Sie uns Typ Anmerkungen hinzufügen zu überprüfen, was falsch ist:

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

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

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

So weit, so gut. Jedoch:

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

ergibt einen Typfehler, da z.B. false hat Typ B a, nicht a, so ist die Anwendung b false schlecht typisiert. Wir können dies umgehen, indem wir ein paar a Argumente x y hinzufügen und die Funktion entsprechend vereinfachen.

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 

Dieser Typ wird überprüft. In ähnlicher Weise können wir bxor überarbeiten, um es Prüfung zu machen Typ:

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

---

Alternativ mit der imprädikative Kirche Codierung von booleans können wir Ihren ursprünglichen Code eingeben machen überprüfen, wie es ist, mit Ausnahme der Zugabe von die relevanten Signaturen. Dies erfordert höherrangige Typen.

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