教堂数字、刚性型和无限型答案

【问题标题】：Church numerals, rigid type and infinite type教堂数字、刚性型和无限型
【发布时间】：2021-10-03 15:32:53
【问题描述】：

我试图实现 Church 数字前置函数 pred，然后我参考了关于 church encodings 的维基百科页面。

据我所知，我写了以下内容

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

我无法弄清楚这两个错误，任何建议都会有所帮助

【问题讨论】：

Church -> Church 表示(forall a . F a) -> (forall a . F a)（对于合适的F），而后者尝试使用forall a . F a -> F a，这是一种完全不同的类型。至少，您需要相同的（rank-2）类型。当您在代码中调用 Church n 时，类型仅为固定（刚性）a 的 F a，而不是所需的 forall a. F a。

标签： haskell types church-encoding

【解决方案1】：

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

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

这同样适用于pred3。

【讨论】：