haskell - Church 编码转换函数无法使用 GADTs 编译

Question

下面的 to_c 函数在使用我想用于此处未显示的不相关代码片段的 GADTs 扩展进行编译时由于类型错误而被拒绝。

newtype Church = Church { unC :: forall a. (a -> a) -> a -> a }
to_c :: Int -> Church
to_c 0 = let f0 f c = c in Church f0
to_c n =
    let fn f c = iterate f c !! n in Church fn

错误信息:

Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope
  This (rigid, skolem) type variable is bound by
    a type expected by the context:
      (a -> a) -> a -> a

  Expected type: (a -> a) -> a -> a
    Actual type: (a0 -> a0) -> a0 -> a0
  In the first argument of ‘Church’, namely ‘fn’

我可以用直接递归的方式重写这个函数，它可以进行类型检查，也可以工作；然而，我很好奇为什么这种迭代方法有缺陷，以及是否可以通过一些巧妙的类型注释来挽救它。

Answer 1

这实际上与 GADT 没有任何关系，只是，-XGADTs 扩展还暗示了 -XMonoLocalBinds，这才是真正的问题所在。它所做的是，因为本地绑定(bind) fn 没有明确的签名，所以它想给它一个不比环境多态的类型......即在这种情况下 根本不是多态的。但当然，它必须是多态的，这样它才能真正用于Church 类型，所以这不好。

您仍然可以提供一个显式多态签名:

{-# LANGUAGE RankNTypes, MonoLocalBinds #-}
newtype Church = Church { unC :: forall a. (a -> a) -> a -> a }
to_c :: Int -> Church
-- to_c 0 = ...  -- the base case is redundant.
to_c n =
    let fn :: (a -> a) -> a -> a
        fn f c = iterate f c !! n
    in Church fn

但更简单的解决方案是根本不进行任何绑定(bind)，这样-XMonoLocalBinds 就不会起作用:

to_c :: Int -> Church
to_c n = Church (\f c -> iterate f c !! n)

...或者，如果您确实进行了绑定(bind)，请在 Church 构造函数中进行，因为那里的环境已经是多态的:

to_c n = Church (let fn f c = iterate f c !! n in fn)