RankNTypes and Church numbers

Question

하스켈에서 교회 숫자를 연구하려고하는데 자연수 인 n은 기본적으로 다음 유형의 함수를 다음과 같은 값으로 적용하는 표현식입니다. n 번에 t을 입력하십시오. 내가 지수를 정의 할 때

zero :: Nat 
zero = \f t -> t 

succ :: Nat -> Nat 
succ n = \f -> f . (n f) 

plus :: Nat -> Nat -> Nat 
plus m n = \f -> (m f) . (n f) 

mult :: Nat -> Nat -> Nat 
mult m n = \f -> m (n f) -- Equal to \f -> (m . n) f 

-- Pointfree version 
mult' :: Nat -> Nat -> Nat 
mult' = (.) 

, 나도 같은 논리를 적용하려고 싶습니다

그 생각으로

type Nat = forall t. (t -> t) -> t -> t 

, 나는 zero이 successor는, 다음과 같은 방법으로 plus, mult 정의 할 수 있습니다 즉, 을 mult mn 번을 1에 적용하여 정의 할 수있었습니다.

이 다음 코드

exp' :: Nat -> Nat -> Nat 
exp' m n = n (mult m) (succ zero) 

에 이르게하지만이 GHC에서 다음과 같은 오류 확인 입력 않습니다

Couldn't match type ‘t’ with ‘t1’ 
    ‘t’ is a rigid type variable bound by 
    the type signature for: 
     exp' :: forall t. Nat -> Nat -> (t -> t) -> t -> t 
    at church.lhs:44:3 
    ‘t1’ is a rigid type variable bound by 
    a type expected by the context: 
     forall t1. (t1 -> t1) -> t1 -> t1 
    at church.lhs:44:17 
    Expected type: ((t -> t) -> t -> t) -> (t -> t) -> t -> t 
    Actual type: Nat -> Nat 

오류가 typechecker이 유형을 인스턴스화되지 말 것

n 적절히 표현식을 입력하려면 t 유형을 다른 유형 (t -> t)으로 인스턴스화해야합니다.

도 내게는 혼란 무슨 다음 코드 typechecks :

exp :: Nat -> Nat -> Nat 
exp m n = n ((.) m) (succ zero) -- replace mult by (.) 

사람의 마음이 문제가 여기에 무엇을 설명하는 것인가? exp'의 첫 번째 정의는 typecheck가 아니라 두 번째 exp typecheks입니까?

감사합니다.

Answer 1

작동하지 않는 이유는 하스켈에서 일반적으로 허용되지 않는 여러 가지 실증적 인스턴스화가 관련되어 있기 때문입니다. 당신이 -XImpredicativeTypes을 설정하면, 당신은 컴파일 얻을 수 있습니다 :

{-# LANGUAGE ImpredicativeTypes #-} 

... 

exp' :: Nat -> Nat -> Nat 
exp' m n = n (mult m) (succ zero) 

두 번째 버전 typechecks을 mult' 더 높은 순위 유형을 가지고 있기 때문에, 그것은 definitionally 동일 (.)로하더라도, 그래서 다르게 진행 유형 검사. (.) 유형이 더 간단하기 때문에 (유형 1) 형식 검사가 더 자주 성공합니다.

GHC 워드 프로세서 ImpredicativeTypes이 작동하지 않으므로 사용에주의해야합니다.

newtype Nat' = N { instN :: Nat } 

exp'' :: Nat -> Nat -> Nat 
exp'' m n = instN $ n (\(N q) -> N $ mult m q) (N $ succC zero) 

---

행동에 impredicative 인스턴스를 참조하려면, 사용자가 입력 사용할 수있는 구멍 :

exp' :: Nat -> Nat -> Nat 
exp' m n = _ (mult m) (succC zero) 

이 유형을보고 일반적인 방법은 newtype 간단한 사용이 주위 얻을 수 forall a . (Nat -> Nat) -> Nat -> (a -> a) -> a -> a이며 (Nat -> Nat) -> Nat -> Nat과 같습니다.n을 배치 했으므로이 유형을 forall a . (a -> a) -> a -> a으로 통합해야합니다. a 변수 유형을 Nat 폴리 상태로 인스턴스화해야합니다.