教会数字，刚性类型和无限类型

Question

我正在尝试实现教会数字前导函数pred教堂,我指的是维基百科页面编码。

根据它，我写了以下

{-# LANGUAGE ScopedTypeVariables, RankNTypes #-}
module Church where
newtype Church = Church { runChurch :: forall a. (a -> a) -> a -> a }
pred1 :: Church -> Church
pred1 (Church n) = Church (f a -> extract (n (g h -> h (g f)) (const a))) where
extract k = k id

哪个类型检查

但是当我尝试使用pred1来更直接地实现它时，

pred2 :: forall a. ((a -> a) -> a -> a) -> (a -> a) -> a -> a
pred2 n = runChurch $ pred1 (Church n)

ghc抱怨

• Couldn't match type ‘a1’ with ‘a’
‘a1’ is a rigid type variable bound by
a type expected by the context:
forall a1. (a1 -> a1) -> a1 -> a1
at Church.hs:11:30-37
‘a’ is a rigid type variable bound by
the type signature for:
pred2 :: forall a. ((a -> a) -> a -> a) -> (a -> a) -> a -> a
at Church.hs:10:1-61
Expected type: (a1 -> a1) -> a1 -> a1
Actual type: (a -> a) -> a -> a
• In the first argument of ‘Church’, namely ‘n’
In the first argument of ‘pred1’, namely ‘(Church n)’
In the second argument of ‘($)’, namely ‘pred1 (Church n)’
• Relevant bindings include
n :: (a -> a) -> a -> a (bound at Church.hs:11:7)
pred2 :: ((a -> a) -> a -> a) -> (a -> a) -> a -> a
(bound at Church.hs:11:1)
|
11 | pred2 n = runChurch $ pred1 (Church n)
|                                     ^

或lambda演算样式

pred3 :: forall a. ((a -> a) -> a -> a) -> (a -> a) -> a -> a
pred3 n f a1 = extract (n (g h -> h (g f)) (const a1)) where
extract k = k id

编译器说

• Occurs check: cannot construct the infinite type:
a ~ (a0 -> a0) -> a
• In the first argument of ‘extract’, namely
‘(n ( g h -> h (g f)) (const a1))’
In the expression: extract (n ( g h -> h (g f)) (const a1))
In an equation for ‘pred3’:
pred3 n f a1
= extract (n ( g h -> h (g f)) (const a1))
where
extract k = k id
• Relevant bindings include
a1 :: a (bound at Church.hs:14:11)
f :: a -> a (bound at Church.hs:14:9)
n :: (a -> a) -> a -> a (bound at Church.hs:14:7)
pred3 :: ((a -> a) -> a -> a) -> (a -> a) -> a -> a
(bound at Church.hs:14:1)
|
14 | pred3 n f a1 = extract (n (g h -> h (g f)) (const a1)) where
|                         ^^^^^^^^^^^^^^^^^^^^^^^^^^

如果我没有指定pred3的类型，则推断的类型是

pred3 :: (((t1 -> t2) -> (t2 -> t3) -> t3) -> (b -> a1) -> (a2 -> a2) -> t4)
-> t1 -> a1 -> t4

这两个错误我实在想不明白，请指教。

Answer 1

想象有人试图打电话给pred2 @Int。然后你最终会试图把(Int -> Int) -> Int -> Int塞进Church，这显然是错误的。要使pred2工作，您需要确保它的第一个参数始终是多态函数，这意味着pred2需要具有rank-2类型。它的定义是很好,所以就替换它的类型签名:

pred2 :: (forall a. (a -> a) -> a -> a) -> (b -> b) -> b -> b

同样适用于pred3。