类型变量将会逃离其作用域

Question

类型变量将会逃离其作用域

20

我正在尝试通过给函数添加一个镜头参数（来自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

- sevo

你使用哪个镜头库？pom、ell、name等类型是什么？你是自己编写了 ./ 还是使用了 xml-lens？ - Zeta

我在这里使用的镜头来自于xml-lens包。 - sevo

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Christian Conkle · Accepted Answer

这里的问题并不在于镜头或xml-lens本身，而是一个更高阶的类型推断问题。

简化测试用例

首先，让我们使用你问题中的有问题的类型创建一个尽可能小的示例。在你的代码中，你将l传递给函数(./)，它期望一个可遍历对象；我将(./)替换为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关于推断和更高阶类型的文档假设如下（摘自GHC 7.8.3 docs）：

对于一个lambda-bound或case-bound变量x，程序员要么为x提供一个显式的多态类型，要么GHC的类型推断将假定x的类型中没有任何foralls。

在我们的例子中，变量l是lambda绑定的，并且它没有明确的多态类型。因此，GHC假定它的类型（错误消息称为t）没有任何foralls。试图将其与forall f。（a0 -> f b0） -> s0 -> f t0 统一起来违反了该假设。

关于类型变量f逃脱其范围的那一部分表明，f需要有一个forall。

顺便说一下，真正的最小示例是这个：

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

f' = \x -> g' x