类型变量将逃避其范围 [英] Type variable would escape its scope

问题描述

我试图通过给它一个镜头参数来重构我的功能（从 xml-lens 包）。我错过了类型量词的一些东西。这是怎么回事？

  * Main>让z name = listToMaybe $ pom ^ .. root ./ ell名称。文本
 * Main> ：t z 
 z ::文字 - >也许文本
 * Main>让z name l = listToMaybe $ pom ^ .. l ./ ell名称。文本
 
< interactive>：13：38：
无法匹配预期的类型'（元素 - > f元素）
  - >文件 - > f将'
'与实际类型't'
相关联，因为类型变量'f'将转义其范围
这个（rigid，skolem）类型变量受到
a类型的限制，上下文：
适用f => （元素→> f元素）→>文件 - > f在< interactive>的文档
：13：38-57 
相关绑定包括
l :: t（绑定在< interactive> 13：12）
z :: Text - > t  - >在'（./）'的第一个参数中，也就是'l'
在'（^ ..）'的第二个参数中， ，即'l / ell名称。文字'
  

有趣的是，这个签名是有效的。

  textFrom :: Text  - >文件 - >镜头'文件元素 - >也许文本
 textFrom name pom ln = listToMaybe $ pom ^ .. ln ./ ell name。文本
  

解决方案

code> xml-lens 直接。它是一个更高级别的类型推断问题。
$ b $ h2>简单测试用例

首先让我们做一个最简单的例子使用问题中的问题类型。在你的代码中，你将 l 传递给函数（./），它需要一个 Traversable的;我将（./）替换为 g ，而忽略了该函数的其余部分。

  g ::遍历刺 - >字符串
 g =未定义
 
  -  f ::遍历s t a b  - >字符串
fl = gl 
  

错误：

 无法匹配预期的类型`（a0  - > f b0） - > s0  - > f t0'
，实际类型为't'
，因为类型变量'f'会跳过它的作用域
这个（rigid，skolem）类型变量受到
a类型的限制，上下文：
 Control.Applicative.Applicative f => （a0→f0）→> s0  - > f t0 
在SO27247620.hs：14：7-9 
相关绑定包括
l :: t（绑定在SO27247620.hs：14：3）
f :: t  - > ;字符串（绑定在SO27247620.hs：14：1）
在`g'的第一个参数中，即'l'
在表达式中：gl 
  

取消注释类型签名可修复它，如同您的问题一样。

让我们将类型签名展开为看看为什么。

  type Traversal stab = forall f。应用f => （a  - > f b） - > s  - > f f（f）f（f）应用f =（a-> f b）→s→f t）→f字符串
  

这里的重点仅仅是 f 有一个更高级的类型，即它包含一个嵌套的 forall ;您需要 RankNTypes 来编写 f 或 g 。

推断更高级别类型

更高级别类型的类型推断并非总是可行。你的问题归结为GHC不能推断出这个更高级的类型;答案基本上是GHC没有承诺它可以这样做。具体来说，GHC关于推理和更高级别类型所做的一个记录假设是，来自 GHC 7.8.3文档：对于一个lambda绑定或绑定case的变量x，程序员要么为x提供一个显式的多态类型，或者GHC的类型推断将假定x的类型没有任何作用。

在我们的例子中，变量 l 是lambda-bound，它没有显式的多态类型。因此，GHC假定它的类型（错误消息调用的是 t ）没有选项。试图用 forall f来统一它。 （a0→f0）→> s0 - > f t0 违反了这个假设。

关于类型变量 f 转义范围的位表明 f


顺便说一句，最简单的例子就是：

pre> g'::（forall a。a） - > b
g'=未定义的

f'= \x - > g'x





I'm trying to refactor my function by giving it a lens argument (from the xml-lens package). I'm missing something about type quantifiers. What is going on here?

*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’

What is interesting, this signature works.

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

解决方案

The problem here isn't with lenses or xml-lens directly. It's a higher-rank type inference issue.

Simplified test case

First let's make a minimal-ish example using the problematic type from your question. In your code, you're passing l to the function (./), which expects a Traversable; I'm replacing (./) with g and leaving out the rest of the function.

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

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

Error:

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

Uncommenting the type signature fixes it, as with your problem.

Let's expand the type signature to see why.

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

The punchline here is simply that f has a higher-rank type, i.e. it contains a nested forall; you need RankNTypes to write either f or g.

Inferring higher-rank types

Type inference for higher-rank types is not always possible. Your problem boils down to "GHC can't infer this higher-rank type"; the answer to that is basically "GHC makes no promise that it can do so."

Specifically, the one documented assumption GHC makes regarding inference and higher-rank types is this, from the GHC 7.8.3 docs:

For a lambda-bound or case-bound variable, x, either the programmer provides an explicit polymorphic type for x, or GHC's type inference will assume that x's type has no foralls in it.

In our example, the variable l is lambda-bound, and it doesn't have an explicit polymorphic type. Therefore GHC assumes that its type (which the error message calls t) has no foralls. Trying to unify it with forall f. (a0 -> f b0) -> s0 -> f t0 violates that assumption.

The bit about type variable f escaping its scope indicates that f needs to have a forall on it.

By the way, the real minimal example is this:

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

f' = \x -> g' x

这篇关于类型变量将逃避其范围的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！