类型变量将逃避其范围

Question

我试图通过给它一个镜头参数来重构我的函数(从xml-lens包中).我错过了关于类型量词的一些东西.这里发生了什么？

*Main> let z name = listToMaybe $ pom ^.. root ./ ell name . text
*Main> :t z
z :: Text -> Maybe Text
*Main> let z name l = listToMaybe $ pom ^.. l ./ ell name . text

<interactive>:13:38:
    Couldn't match expected type ‘(Element -> f Element)
                                  -> Document -> f Document’
                with actual type ‘t’
      because type variable ‘f’ would escape its scope
    This (rigid, skolem) type variable is bound by
      a type expected by the context:
        Applicative f => (Element -> f Element) -> Document -> f Document
      at <interactive>:13:38-57
    Relevant bindings include
      l :: t (bound at <interactive>:13:12)
      z :: Text -> t -> Maybe Text (bound at <interactive>:13:5)
    In the first argument of ‘(./)’, namely ‘l’
    In the second argument of ‘(^..)’, namely ‘l ./ ell name . text’

有趣的是,这个签名有效.

textFrom :: Text -> Document -> Lens' Document Element -> Maybe Text
textFrom name pom ln = listToMaybe $ pom ^.. ln ./ ell name . text

Answer 1

这里的问题不是透镜或xml-lens直接.这是一个更高级别的类型推断问题.

简化测试用例

首先,让我们使用您问题中的有问题的类型制作一个最小的例子.在你的代码中,你要传递l给函数(./),它需要一个Traversable; 我更换(./)与g和离开该功能的其余部分.

g :: Traversal s t a b -> String
g = undefined

-- f :: Traversal s t a b -> String
f l = g l

错误:

Couldn't match expected type `(a0 -> f b0) -> s0 -> f t0'
            with actual type `t'
  because type variable `f' would escape its scope
This (rigid, skolem) type variable is bound by
  a type expected by the context:
    Control.Applicative.Applicative f => (a0 -> f b0) -> s0 -> f t0
  at SO27247620.hs:14:7-9
Relevant bindings include
  l :: t (bound at SO27247620.hs:14:3)
  f :: t -> String (bound at SO27247620.hs:14:1)
In the first argument of `g', namely `l'
In the expression: g l

取消注释类型签名可以修复它,就像您的问题一样.

让我们扩展类型签名以了解原因.

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

f :: (forall f. Applicative f => (a-> f b) -> s -> f t) -> String

这里的妙语只是f具有更高级别的类型,即它包含嵌套forall; 你需要RankNTypes写f或者g.

推断更高等级的类型

高阶类型的类型推断并不总是可行的.你的问题归结为"GHC无法推断出这种更高级别的类型"; 对此的答案基本上是"GHC不承诺它可以这样做."

具体而言,从GHC 7.8.3文档中,GHC对推理和更高级别类型做出的一个记录的假设是这样的:

对于lambda-bound或case-bound变量x,要么程序员为x提供显式多态类型,要么GHC的类型推断将假设x的类型中没有foralls.

在我们的示例中,变量l是lambda绑定的,并且它没有显式的多态类型.因此,GHC假定其类型(错误消息调用的t)没有任何内容.试图统一它forall f. (a0 -> f b0) -> s0 -> f t0违反了这个假设.

关于类型变量f转义其范围的位表明f需要有一个forall.

顺便说一句,真正的最小例子是这样的:

g' :: (forall a. a) -> b
g' = undefined

f' = \x -> g' x