4

每什么是 skolems？，这有效：

{-# LANGUAGE ExistentialQuantification #-}

data AnyEq = forall a. Eq a => AE a

reflexive :: AnyEq -> Bool
reflexive (AE x) = x == x

但是为什么不这样：

reflexive2 :: AnyEq -> Bool
reflexive2 ae = x == x
  where
  AE x = ae

（或类似的版本let）。它产生的错误包括：

Couldn't match expected type ‘p’ with actual type ‘a’
        because type variable ‘a’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a pattern with constructor: AE :: forall a. Eq a => a -> AnyEq,
        in a pattern binding
        at Skolem.hs:74:4-7

是否可以通过添加一些类型声明来使其工作（有点像该问题s :: forall a. I a -> String中示例的解决方案withContext）。我觉得我想在Eq x某个地方添加一个。

我（可能是幼稚的）对reflexive工作原理的理解如下：

  • 它需要一个 type 的值AnyEq。这在其中嵌入了任何类型的值，只要它是Eq. 这种内部类型在的类型签名中并不明显，并且在编译reflexive时是未知的。reflexive
  • 该绑定生成(AE x) = ae了x一个未知类型的值，但已知它是Eq. （所以就像变量 x 和 y 一样myEq :: Eq a => a -> a -> Bool; myEq x y = x == y）
  • ==基于隐含的类约束，操作员很高兴。

我想不出为什么reflexive2不做同样的事情，除了像“单态限制”或“单局部绑定”这样的事情，有时会让事情变得很奇怪。我尝试使用 and 的所有组合进行编译NoMonomorphismRestriction，NoMonoLocalBinds但无济于事。

谢谢。

4

1 回答 1

3

所以我想我在文档中找到了答案（所有地方！）。这说明：

  • 您不能在 let 或 where 组绑定中对存在量化的构造函数进行模式匹配
  • 这种限制的原因实际上是一种实现
  • 我们会看到它有多烦人

还有一个取消限制的请求（尽管这似乎有点挑战性）。

就个人而言，现在我想我明白了，它并不那么烦人。但我确实认为生成的错误消息具有误导性（因为我不认为问题是范围泄漏），所以会要求对其进行更改。（如果生成的错误消息有对文档的引用，那也很好，所以也会通过询问来推动我的运气。）

感谢大家的评论，如果您认为我有一些错误，请告诉我。大卫。

于 2020-07-30T10:32:06.387 回答