haskell의 부울 논리 및 유형

Question

현재 대학을 위해 하스켈을 운영 중입니다.

이

true::t -> t1 -> t 
true = (\x y -> x) 

false::t -> t1 -> t1 
false = (\x y -> y) 

-- Implication 
(==>) = (\x y -> x y true) 

작업은 함수 (==>)의 종류를 결정하는 것입니다 : 다음 하스켈 코드를 감안할 때. GHCi는 (==>) :: (t1 -> (t2 -> t3 -> t2) -> t) -> t1 -> t이라고 말합니다.

나는 평가 순서는 (유형이 동일하게 유지로) 다음과 같은 것을 볼 수 있습니다 : (x y)에

이

(==>) = (\x y -> (x y) true) 

그래서 기능 true 표준시 인수.

왜 결과 유형 t가 첫 번째 인수의 결과에 바인딩되고 GHCi가 (==>) 유형을 결정하는지 설명 할 수 있습니까?

Answer 1

첫째, 더 나은 개요를 제공하기 위해,

type True t f = t -> f -> t 
type False t f = t -> f -> f 

는 이제 \x y -> x y true :: r에, 우리가 가지고있는 의미 r의 결과를 부르 자, 따라서

x y :: True t f -> r 

그래서 x :: y -> True t f -> r 및

그

(==>) :: (y -> True t f -> r) -> y -> r 

, 확장형 True 다시

(==>) :: (y -> (t->f->t) -> r) -> y -> r