반복되는 증분을 사용하여 유형화 된 교회 숫자에 더하기를 구현할 수 있습니까?

Question

형식이없는 언어에서도 가능하지만 반복 증분으로 추가를 정의하는 방법을 찾을 수 없습니다. 여기 내 코드입니다 : 내가 add2 얻을

{-# LANGUAGE RankNTypes #-} 
type Church = forall a . (a -> a) -> (a -> a) 

zero :: Church 
zero = \f -> id 

inc :: Church -> Church 
inc n = \f -> f . n f 

-- This version of addition works 
add1 :: Church -> Church -> Church 
add1 n m = \f -> n f . m f 

-- This version gives me a compilation error 
add2 :: Church -> Church -> Church 
add2 n m = n inc m 

컴파일 오류가

Couldn't match type `forall a1. (a1 -> a1) -> a1 -> a1' 
        with `(a -> a) -> a -> a' 
    Expected type: ((a -> a) -> a -> a) -> (a -> a) -> a -> a 
     Actual type: Church -> (a -> a) -> a -> a 
    In the first argument of `n', namely `inc' 
    In the expression: n inc m 
    In an equation for `add2': add2 n m = n inc m 

입니다 왜이 오류가? 은 그 ((a->a) -> a -> a)의 동의어가 아닙니까?

Answer 1

추가 유형의 특수 효과가 추가 되더라도 코드를 입력 할 수 없지만 충분히 영리하지 못했습니다. (I도. ImpredicativeTypes을 추가하는 시도) 여기 문제가 정의에

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

이

a 만 (즉, 내부 foralls없이) 순위 - 0 유형으로 인스턴스화 할 수 자체가하지 않은 Church 것을 생각 . 따라서이 방법으로 정의 된 교회 번호를 inc에 적용 할 수 없습니다.

그러나 다소 장황한 해결 방법이 있지만 다르게 작동하게 만들 수 있습니다. Church을 형식이 아닌 newtype으로 만들어 외부에서 단일 형태로 처리 할 수 ​​있도록합니다. 다음은 모두 작동합니다 :

{-# LANGUAGE RankNTypes #-} 
newtype Church = Church { runChurch :: forall a . (a -> a) -> (a -> a) } 

zero :: Church 
zero = Church (\f -> id) 

inc :: Church -> Church 
inc n = Church (\f -> f . runChurch n f) 

add2 :: Church -> Church -> Church 
add2 n = runChurch n inc