haskell – 类型错误与rank-n类型和镜头

2023年11月4日 220次阅读

我有一个简单的多态数据类型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)’但我不明白为什么.

为什么这不能编译,我能做些什么来使这样的东西工作？

最佳答案 你想[bar]有类型[forall c.镜头'(Foo c)c],但它实际上有类型forall f c. Functor f => [(c – > f c) – > Foo c – > f(Foo c)].编译器推断后一种类型的签名,因为它是预测性的.您可以在(im)预测类型的技术细节上找到
resources.简而言之,类型推断在存在不可预测的类型时是不可判定的 – 因此类型签名成为强制性的 – 因此默认情况下它们是不允许的.不可预测的类型是在类型构造函数(如[])中发生forall的类型.

您可以通过简单地指定类型签名并启用ImpredicativeTypes来强制[bar]拥有前一种类型.地图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])

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

点赞