Church 인코딩 변환 기능이 GADT로 컴파일되지 않습니다.

Question

여기에 나와 있지 않은 관련없는 코드 조각에 사용할 GADT 확장 프로그램으로 컴파일 할 때 유형 오류로 인해 아래의 to_c 기능이 거부됩니다.

newtype Church = Church { unC :: forall a. (a -> a) -> a -> a } 
to_c :: Int -> Church 
to_c 0 = let f0 f c = c in Church f0 
to_c n = 
    let fn f c = iterate f c !! n in Church fn 

오류 메시지 :

Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope 
    This (rigid, skolem) type variable is bound by 
    a type expected by the context: 
     (a -> a) -> a -> a 

    Expected type: (a -> a) -> a -> a 
    Actual type: (a0 -> a0) -> a0 -> a0 
    In the first argument of ‘Church’, namely ‘fn’ 

내가 일을 또한 확인하고 입력합니다 직접 재귀 스타일 기능을 다시 작성할 수 있습니다; 그러나이 반복적 인 접근 방식이 결함이 있는지, 그리고 그것이 영리한 유형의 주석으로 복구 될 수 있는지 궁금했습니다.

Answer 1

이것은 실제로 GADT와 아무런 관련이 없습니다. -XGADTs 확장은 -XMonoLocalBinds을 의미하며 실제 문제입니다. 로컬 바인딩 fn에 명시적인 서명이 없으므로 환경보다 더 이상 다형성이없는 유형을 지정하려고합니다. 즉이 경우 다형성이 전혀 없습니다입니다. 그러나 은 유형에서 실제로 사용할 수 있으므로이 다형성이어야하므로 좋지 않습니다.

당신은 여전히 ​​명시 적 다형성 서명을 제공 할 수 있습니다 :

{-# LANGUAGE RankNTypes, MonoLocalBinds #-} 
newtype Church = Church { unC :: forall a. (a -> a) -> a -> a } 
to_c :: Int -> Church 
-- to_c 0 = ... -- the base case is redundant. 
to_c n = 
    let fn :: (a -> a) -> a -> a 
     fn f c = iterate f c !! n 
    in Church fn 

을하지만 쉬운 해결책은 단지 모든 바인딩, 다음 -XMonoLocalBinds 플레이에 오지 않는 을하지 않는 것입니다 :

당신이 결합하게 할 경우 환경이 이미 다형성이 있기 때문에

to_c :: Int -> Church 
to_c n = Church (\f c -> iterate f c !! n) 

... 나,의 Church 생성자 내에서 그것을 할 :

to_c n = Church (let fn f c = iterate f c !! n in fn)