haskell - 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)] .编译器推断后一种类型签名，因为它是预测性的。您可以找到resources关于(im)预测类型的技术细节。简而言之，在存在不可预测类型的情况下，类型推断是不可判定的——因此类型签名成为强制性的——因此默认情况下它们是不允许的。不可预测的类型是 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 它为所有常见的镜头类型声明了新类型，以便您可以在容器中拥有镜头。在这个特定的用例中，这实际上对您没有帮助，因为您还需要 c在 Lens' (Foo c) c绑定(bind)在列表构造函数中，但通常很有用。