haskell에서 교회 숫자를 뺍니다.

Question

하스켈에서 교회 숫자를 구현하려하지만 사소한 문제가 발생했습니다. 하스켈은 수표를 발생

와 무한한 종류의 불평 : 무한 유형 만들 수 없습니다 : t = (t -> T1) - 나는 노력과 뺄셈을 할 때> T2

-> (T1 -> T2)를. 나는 나의 람다 미적분학이 유효하다는 것을 99 % 긍정적이다. (그렇지 않다면 말해라.). 내가 알고 싶은 것은, haskell이 제 기능을 수행하도록 할 수있는 일이 있는지입니다.

module Church where 

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

makeChurch :: Int -> (Church a) 
makeChurch 0 = \f -> \x -> x 
makeChurch n = \f -> \x -> f (makeChurch (n-1) f x) 

numChurch x = (x succ) 0 

showChurch x = show $ numChurch x 

succChurch = \n -> \f -> \x -> f (n f x) 

multChurch = \f2 -> \x2 -> \f1 -> \x1 -> f2 (x2 f1) x1 

powerChurch = \exp -> \n -> exp (multChurch n) (makeChurch 1) 

predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u) 

subChurch = \m -> \n -> (n predChurch) m 

Answer 1

단지 지정되지 않은 버전의 predChurchdoesn't work in simply typed lambda calculus의 정의. Haskell here에서 작동하는 predChurch 버전을 찾을 수 있습니다.

Answer 2

문제는 predChurch이 너무 많아서 Hindley-Milner 유형 추론에 의해 정확하게 추론 될 수 없다는 것입니다. 예를 들어 다음과 같이 쓰고 싶습니다.

predChurch :: Church a -> Church a 
predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u) 

이 유형은 올바르지 않습니다. Church a은 첫 번째 인수로 a -> a을 취하지 만, n 두 개의 인수 함수를 전달합니다. 분명히 유형 오류입니다.

Church a은 교회 숫자를 올바르게 특성 지정하지 못합니다. 교회 숫자는 단순히 숫자를 나타냅니다 - 그 유형 매개 변수는 무엇을 의미합니까? 예 :

foo :: Church Int 
foo f x = f x `mod` 42 

typechecks이지만 foo은 분명히 교회 숫자가 아닙니다. 유형을 제한해야합니다. 교회 번호는 a에 해당하며 구체적으로 a이 아닙니다. 올바른 정의는 다음과 같습니다

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

당신은이 같은 유형을 사용할 수 있도록 파일의 맨 위에 {-# LANGUAGE RankNTypes #-}이 필요합니다. 높은 순위 유형은 힌들리 - 밀너에 의해 inferrable되지 않기 때문에

predChurch :: Church -> Church 
-- same as before 

당신 이 여기 유형 서명을 제공해야합니다 :

이제 우리는 우리가 기대하는 유형의 서명을 제공 할 수 있습니다. 그러나

, 우리는 subChurch 또 다른 문제를 구현하기 위해 이동 발생 :

Couldn't match expected type `Church' 
     against inferred type `(a -> a) -> a -> a' 

내가 이런 이유를 100 % 확신, 나는 forall 너무 후한 typechecker에 의해 전개되고있다 생각합니다. 그것은 나를 놀라게하지 않는다. 더 높은 순위 유형은 컴파일러에게 제시하는 어려움 때문에 조금 부서지기 쉽습니다.게다가 우리는 추상화에 type을 사용해서는 안되며, 우리는 newtype을 사용해야합니다 (이는 더 많은 정의의 유연성을 제공하고, typechecking으로 컴파일러를 돕고, 우리가 추상화의 구현을 사용하는 곳을 표시 함) :

: subChurch와

predChurch = \n -> Church $ 
    \f -> \x -> unChurch n (\g -> \h -> h (g f)) (\u -> x) (\u -> u) 

같은 :

newtype Church = Church { unChurch :: forall a. (a -> a) -> (a -> a) } 

그리고 우리는 롤하고 필요 풀다 predChurch을 수정해야

subChurch = \m -> \n -> unChurch n predChurch m 

하지만 더 이상 유형 서명이 필요하지 않습니다. 유형을 다시 추론하기에 충분한 정보가 롤/언 롤에 있습니다.

새 추상화를 만들 때 항상 newtype 초를 권장합니다. 일반 type 동의어는 내 코드에서 매우 드뭅니다.

Answer 3

동일한 문제가 발생했습니다. 그리고 형식 서명을 추가하지 않고 그것을 해결했습니다.

conscar을 SICP에서 복사 한 해결책이 있습니다.

cons x y = \m -> m x y 
car z = z (\p q -> p) 
cdr z = z (\p q -> q) 

next z = cons (cdr z) (succ (cdr z)) 
pred n = car $ n next (cons undefined zero) 

sub m n = n pred m 

전체 소스는 here입니다.

sub m n = n pred m을 작성한 후 정말 놀랐습니다. 유형 오류없이 ghci에서로드했습니다.

하스켈 코드가 간결합니다! :-)