rank-n 类型和镜头的类型错误

Question

我有一个简单的多态数据类型Foo

{-# LANGUAGE TemplateHaskell #-}
import Control.Lens

data Foo c = 
    Foo {
        _bar :: c,
        _baz :: c,
        _quux :: c
    }   

makeLenses ''Foo

当然，生成的镜头在c 中是多态的。来自 GHCi 的类型是：

*Main> :t bar
bar :: Functor f => (c0 -> f c0) -> Foo c0 -> f (Foo c0)

我创建了一个数据类型Blah 来环绕镜头。这在简单的情况下可以正常工作（当然，使用 RankNTypes 扩展名）：

data Blah = Blah (forall c . Lens' (Foo c) c)

orange :: Blah
orange = Blah bar

但是任何稍微复杂的东西都不起作用，例如

cheese :: [Blah]
cheese = map Blah [bar]

最后一段代码给出了来自 GHC 的错误：

    Couldn't match type ‘(c0 -> f0 c0) -> Foo c0 -> f0 (Foo c0)’
                  with ‘forall c (f :: * -> *).
                        Functor f =>
                        (c -> f c) -> Foo c -> f (Foo c)’
    Expected type: ((c0 -> f0 c0) -> Foo c0 -> f0 (Foo c0)) -> Blah
      Actual type: (forall c. Lens' (Foo c) c) -> Blah
    In the first argument of ‘map’, namely ‘Blah’
    In the expression: map Blah [bar]

forall c f . 似乎从 ‘(c0 -> f0 c0) -> Foo c0 -> f0 (Foo c0)’ 中消失了，但我不明白为什么。

为什么这不能编译，我该怎么做才能让这样的东西工作？

Answer 1

您希望[bar] 具有[forall c . Lens' (Foo c) c] 类型，但它实际上具有forall f c . Functor f => [(c -> f c) -> Foo c -> f (Foo c)] 类型。编译器推断后一种类型签名，因为它是谓词。您可以在 (im) 预测类型的技术细节上找到 resources。简而言之，在存在不可预测类型的情况下，类型推断是不可判定的——因此类型签名成为强制性的——因此默认情况下它们是不允许的。不可预测类型是在类型构造函数中出现forall 的类型（如[]）。

您可以强制[bar] 使用前一种类型，只需指定该类型签名并启用ImpredicativeTypes。 map Blah 也是如此 - 它也有一个不可预测的类型，因此您还需要手动指定它。

bar' :: [forall c . Lens' (Foo c) c]
bar' = [bar] 

mapBlah :: [forall c . Lens' (Foo c) c] -> [Blah]
mapBlah = map Blah 

然后进行以下类型检查：

> mapBlah bar'

甚至

> (map Blah :: [forall c . Lens' (Foo c) c] -> [Blah]) 
    ([bar] :: [forall c . Lens' (Foo c) c])

事实上，处理不可预测类型的问题，lens 包括模块Control.Lens.Reified，它为所有常见的镜头类型声明了新类型，以便您可以在容器中拥有镜头。在这个特定的用例中，这实际上对您没有帮助，因为您还希望将Lens' (Foo c) c 中的c 绑定在列表构造函数中，但它通常很有用。