是否可以使用迭代递增在类型化的教会数字上实现添加？

Question

我无法找到一种方法来将加法定义为重复递增,尽管这在无类型语言中是可能的.这是我的代码:

{-# 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

我得到的编译错误add2是

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

为什么这是一个错误？那不是Church同义词((a->a) -> a -> a)吗？

Answer 1

无论我添加了哪种类型的注释,我都无法输入您的代码,尽管我可能不够聪明.(我也尝试过添加ImpredicativeTypes.)我认为这里的问题是在定义中

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

a只能用rank-0类型实例化(即没有内部的foralls),它Church本身不是.因此,您不能将以这种方式定义的教会数字应用于您的inc.

但是,有一个相对简单的解决方法略显冗长,但是使一切工作都很好:成为Church一个新类型而不是一个类型,这样它就可以被视为来自外部的单形.以下都有效:

{-# 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