具有排名-n类型和镜头的类型错误

Question

具有排名-n类型和镜头的类型错误

4

我有一个简单的多态数据类型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)' 中消失了，但我不明白为什么。

为什么这个代码无法编译？有什么方法可以让它正常工作吗？

- tjhance

嗯，我不确定我能给出足够正确的解释来证明完整的答案，但似乎这是与“Blah”的作用域问题有关。如果你将forall c.移到构造函数之外，如data Blah = forall c. Blah (Lens' (Foo c) c)，那么map Blah将会通过类型检查，但map Blah [bar]则不会。如果你展开Lens'类型并手动执行data Blah = forall c f. Functor f => Blah ((c -> f c) -> Foo c -> f (Foo c))，那么你就有了:t map Blah为Functor f => [(c -> f c) -> Foo c -> f (Foo c)] -> [Blah]以及:t [bar, baz]为[(c -> f c) -> Foo c -> f (Foo c)]... - bheklilr

但是它无法统一 map Blah [bar, baz] 中的 Functor 约束。我认为这是因为 Blah 构造函数对类型检查器隐藏了太多的信息，所以它无法确定如何整合 Functor 约束。如果镜头类型没有约束，那么它可能会真正起作用。 - bheklilr

我唯一能让任何东西进行类型检查的方法是将类型参数添加到 Blah 中，如 data Blah f c where Blah :: Functor f => ((c -> f c) -> Foo c -> f (Foo c)) -> Blah f c，然后你可以执行 map Blah [bar, baz] 并具有类型 Functor f => [Blah f c]，但这并不意味着没有隐藏这些类型变量的方法。我认为这里最重要的是 f，因为它有一个 Functor 约束。编译器必须选择一个 Functor 实例，但没有办法只选择一个，所以它无法通过类型检查。 - bheklilr

2

你想让 [bar] 的类型为 [forall c . Lens' (Foo c) c]，但它实际上的类型是 Functor f => [(c0 -> f c0) -> Foo c0 -> f (Foo c0)]。你可以通过简单地指定该类型签名来强制 [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' 也将通过类型检查。 - user2407038

2

顺便说一句，我不建议使用不可预测的类型 - 您将不得不为每个不可预测的类型编写类型签名，而它并不能给您带来太多的优势。 - user2407038

@user2407038：你能把那个放到答案里吗？这样更容易阅读，而且回答了问题。谢谢！ - Tikhon Jelvis

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- user2407038 · Accepted Answer

您希望[bar]的类型为[forall c . Lens' (Foo c) c]，但实际上它的类型是forall f c . Functor f => [(c -> f c) -> Foo c -> f (Foo c)]。编译器推断后者类型签名是因为它是“预测性”的。您可以在这里找到关于（非）预测类型的技术细节资源。简而言之，在存在非预测类型的情况下，类型推断是不可判定的，因此类型签名变得强制性，并且默认情况下不允许使用。非预测类型是指forall出现在类型构造函数（如[]）中的类型。

您可以通过简单地指定该类型签名并启用ImpredicativeTypes来强制[bar]具有前面的类型。对于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 类型声明了新类型，从而使您可以在容器中使用 lens。实际上，在这种特定的用例中，这并不能帮助您，因为您还希望在列表构造函数内绑定到 Lens' (Foo c) c 中的 c，但是它通常很有用。