下面的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’
我可以用直接递归样式重写函数,它将进行类型检查并且也可以工作;但是,我很好奇为什么这种迭代方法有缺陷,以及它是否可以用一些聪明的类型注释来挽救。
这与GADT没有任何关系,只有,-XGADTs
扩展也暗示-XMonoLocalBinds
,这就是真正的问题。它的作用是,因为本地绑定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
但更简单的解决方案就是不要做任何绑定,然后-XMonoLocalBinds
不会发挥作用:
to_c :: Int -> Church
to_c n = Church (\f c -> iterate f c !! n)
...或者,如果您确实进行了绑定,请在Church
构造函数中执行此操作,因为环境已经是多态的:
to_c n = Church (let fn f c = iterate f c !! n in fn)