Тип соответствует только внутри функции в haskell

Question

Я новичок в haskell и пытаюсь внедрить церковную кодировку для натуральных чисел, как объясняется в this guide.

{-# LANGUAGE RankNTypes #-} 

newtype Chur = Chr (forall a. (a -> a) -> (a -> a)) 

zero :: Chur 
zero = Chr (\x y -> y) 

-- church to int 
c2i :: Chur -> Integer 
c2i (Chr cn) = cn (+ 1) 0 

-- this works 
i1 = c2i zero 
-- this doesn't 
i2 = zero (+ 1) 0 

Для i2 я получаю несоответствие типов:

Couldn't match expected type ‘(Integer -> Integer) -> Integer -> t’ 
      with actual type ‘Chur’ 
Relevant bindings include i2 :: t (bound at test.hs:14:1) 
The function ‘zero’ is applied to two arguments, 
but its type ‘Chur’ has none 
In the expression: zero (+ 1) 0 
In an equation for ‘i2’: i2 = zero (+ 1) 0 

Как прийти Chur может принимать аргументы, когда обернутый в функции, но не может без него?

Answer 1

Chur не принимает никаких аргументов, когда обернутый в функции - функции, завернутые в Chur делает:

c2i (Chr cn) = cn (+ 1) 0 

Здесь cn функция завернуты внутри Chur.

Вы можете использовать метод подстановки, чтобы увидеть, что происходит:

c2i zero 
==> c2i (Chr (\x y -> y)) 
==> (\x y -> y) (+ 1) 0 
==> 0 

Но

zero (+ 1) 0 
==> (Chr (\x y -> y)) (+ 1) 0 

, который не работает, так как (Chr (\x y -> y)) не является функцией.

Если бы ты написал

c2i :: Chur -> Integer 
c2i cn = cn (+ 1) 0 

вы бы видели подобную ошибку.