왜 형식 서명이 이렇게 생겼습니까? (교회 번호를 Int로 변환)

Question

저는 하스켈을 배우고 교회 번호를 Int로 변환하는 함수를 작성하려고합니다. 내 코드는 형식 서명을 쓰지 않는 경우에만 작동합니다.

type Church a = (a -> a) -> a -> a 

zero :: Church a 
zero s z = z 

c2i :: Church a -> Int -- This line fails 
c2i x = x (+1) 0 

나는 :t c2i

c2i :: (Num a1, Num a) => ((a -> a) -> a1 -> t) -> t 

사용 c2i의 오른쪽 유형 서명을 가지고 있지만 그것이 왜 궁금하네요? 당신이 c2i 서명에 a를 사용하는 경우

Answer 1

은, 그것은 어떤a와 함께 작동한다. 즉, a은 호출자에 의해 선택됩니다. 구체적으로는, 그것은 a = String가, 다형성 타입이 무효 인 경우에 코드가 작동하지 않기 때문에

c2i :: Church String -> Int 
-- that is 
c2i :: ((String -> String) -> String -> String) -> Int 

와 함께 작동한다.

형식을 추가하지 않으면 컴파일러에서 코드를 작동시키는 일부 형식을 유추 할 수 있습니다. 더 간단한 형태가 될 수있다 :

c2i :: Church Int -> Int 

하거나, 후자의 경우 몇 확장,

c2i :: (forall a. Church a) -> Int 

을 활성화 한 후, 우리는 a가되지 발신자가, c2i에 의해 선택되는 것을 지정한다. 대신 호출자는 다형 유형이 있어야하는 인수를 전달해야합니다. 즉 Church String이 아니라 a에 대해 Church a을 전달해야합니다.

달리, 하나도

type Church = forall a . (a->a)->a->a 

선언하고 만 다형성 값 주위에 전달한다.