하스켈에있는 교회에서 인코딩 된 불린 xor

Question

저는 xor 용 람다 식을 구현하려고합니다. 그러나 나는 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

입력 된 환경에서주의해야합니다. 귀하의 람다 - 용어는 untyped 설정에서 잘 작동하지만, 입력 된 하나 조정할 필요합니다.

교회 불법 행위에 대한 유형을 정의해야합니다. 다음의 파라 메트릭 monomorphic 타입을 선택합시다.

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 

지금까지. 그러나 :

은 예를 들어. 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 재 작업을 할 수 있습니다 : 논리 값의 impredicative 교회 인코딩을 사용하여, 또는

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

---

을, 우리는 추가를 제외하고, 그대로 원래의 코드를 확인 입력 할 수 있습니다 관련 유형 서명. 여기에는 높은 순위 유형이 필요합니다.

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