在haskell中减去教堂数字

Question

我试图在Haskell中实现教堂数字,但我遇到了一个小问题.Haskell抱怨无限类型

发生检查:无法构造无限类型:t =(t - > t1) - >(t1 - > t2) - > t2

当我尝试做减法时.我99%肯定我的lambda演算是有效的(虽然如果不是,请告诉我).我想知道的是,我能做些什么来让haskell与我的功能一起工作.

module Church where

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

makeChurch :: Int -> (Church a)
makeChurch 0 = \f -> \x -> x
makeChurch n = \f -> \x -> f (makeChurch (n-1) f x)

numChurch x = (x succ) 0

showChurch x = show $ numChurch x

succChurch = \n -> \f -> \x -> f (n f x)

multChurch = \f2 -> \x2 -> \f1 -> \x1 -> f2 (x2 f1) x1

powerChurch = \exp -> \n -> exp (multChurch n) (makeChurch 1)

predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

subChurch = \m -> \n -> (n predChurch) m

Answer 1

问题是,predChurch是太多态性由辛德米尔纳类型推断正确推断.例如,写作很有诱惑力:

predChurch :: Church a -> Church a
predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

但这种类型不正确.A Church a将第一个参数作为第一个参数a -> a,但是您传递的n是两个参数函数,显然是一个类型错误.

问题是Church a没有正确表征教会数字.教会数字只代表一个数字 - 这个类型参数究竟意味着什么？例如:

foo :: Church Int
foo f x = f x `mod` 42

那种说法,但foo肯定不是教会的数字.我们需要限制类型.教会数字需要适用于任何 a,而不仅仅是特定的a.正确的定义是:

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

您需要{-# LANGUAGE RankNTypes #-}在文件的顶部启用这样的类型.

现在我们可以给出我们期望的类型签名:

predChurch :: Church -> Church
-- same as before

你必须在这里给出一个类型签名,因为Hindley-Milner不能推断出更高等级的类型.

但是,当我们去实施subChurch另一个问题时:

Couldn't match expected type `Church'
       against inferred type `(a -> a) -> a -> a'

我不是百分之百地确定为什么会发生这种情况,我认为这forall是由类型检查员过于宽松的展开.不过我并不感到惊讶; 较高级别的类型可能有点脆弱,因为它们给编译器带来了困难.此外,我们不应该用type一个抽象的,我们应该使用newtype(这使我们在定义更多的灵活性,有助于类型检查的编译器,标志着我们用抽象的实现的地方):

newtype Church = Church { unChurch :: forall a. (a -> a) -> (a -> a) }

我们必须修改predChurch以根据需要滚动和展开:

predChurch = \n -> Church $ 
    \f -> \x -> unChurch n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

与subChurch:相同:

subChurch = \m -> \n -> unChurch n predChurch m

但是我们不再需要类型签名了 - 滚动/展开中有足够的信息可以再次推断类型.

newtype在创建新抽象时我始终建议使用s.type在我的代码中,常规同义词非常罕见.

Answer 2

这个定义predChurch 在简单类型的lambda演算中不起作用,仅在非类型化版本中.你可以predChurch在这里找到一个适用于Haskell 的版本.