我找不到将加法定义为重复递增的方法,尽管这在无类型语言中是可能的。这是我的代码:
{-# 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)
的同义词吗? 最佳答案
无论我添加了什么额外的类型注释,我都无法输入您的代码,尽管我可能不够聪明。 (我也尝试添加 ImpredicativeTypes
。)
我认为这里的问题是在定义中
type Church = forall a. (a -> a) -> (a -> a)
a
只能用 rank-0 类型(即内部没有 foralls)实例化,而 Church
本身不是。因此,您不能将以此方式定义的 Church 数字应用于 inc
。然而,有一个相对简单的解决方法,它稍微有点冗长,但其他方面都可以很好地工作:将
Church
变成 newtype 而不是类型,这样它就可以从外部被视为单态。以下所有工作:{-# 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
关于haskell - 是否可以使用迭代增量对键入的 Church 数字实现加法?,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/23705936/