为什么 makeLenses 不为某些量化的构造函数派生透镜？

Question

我正在尝试为稍微复杂的 GADT 制作镜头，但发现它不想为我的一位构造函数生成镜头。代码如下所示：

{-# LANGUAGE GADTs, RankNTypes, TemplateHaskell, KindSignatures, DataKinds #-}

import Control.Lens
import GHC.TypeNats

data Variant (m :: Nat) where
  VariantA :: Variant 42

data Stuff where
  Foo :: { _foo :: Int } -> Stuff
  Bar :: forall t. { _bar :: String } -> Stuff
  Baz :: forall m. { _baz :: Variant m } -> Stuff

$(makeLenses ''Stuff)

我发现这会生成镜头 foo 和 bar，但不会生成 baz。这似乎与 baz 的约束和种类签名 Variant m 有关。为什么我买不到 baz 的镜头？

我看到在 https://github.com/ekmett/lens/issues/409 末尾添加了一些对存在量化记录构造函数的支持，但想知道这是否是一个进一步的 lens 问题。

Answer 1

问题不在于 makeLenses。问题是你真的不能为_baz写一个Traversal，甚至Setter。让我们看看当您尝试编写 Traversal:

时会发生什么

baz :: Traversal' Stuff (Variant m)
baz f (Baz v) = _
baz _f s = pure s

GHC 说：

LensGADT.hs:19:17: error:
    • Found hole: _ :: f Stuff
      Where: ‘f’ is a rigid type variable bound by
               the type signature for:
                 baz :: forall (m :: Nat). Traversal' Stuff (Variant m)
               at LensGADT.hs:18:1-35
    • In the expression: _
      In an equation for ‘baz’: baz f (Baz v) = _
    • Relevant bindings include
        v :: Variant m1 (bound at LensGADT.hs:19:12)
        f :: Variant m -> f (Variant m) (bound at LensGADT.hs:19:5)
        baz :: (Variant m -> f (Variant m)) -> Stuff -> f Stuff
          (bound at LensGADT.hs:19:1)
      Constraints include Applicative f (from LensGADT.hs:18:1-35)
   |
19 | baz f (Baz v) = _
   |                 ^

你看到问题了吗？对于某些 m，我们得到了一个 Variant m -> f (Variant m) 类型的函数，并且对于某些（可能不同的）m1，我们有一个 Variant m1 类型的值。我们不可能应用该功能！如果您尝试编写 setter.

，则会出现完全相同的问题

你能做的最好的是：

baz1 :: Applicative f => (forall m. Variant m -> f (Variant m)) -> Stuff -> f Stuff
baz1 f (Baz v) = Baz <$> f v
baz1 _f s = pure s

或这个（相同的代码，类型略有不同）：

baz2 :: Applicative f => (forall m. Variant m -> f (Variant n)) -> Stuff -> f Stuff
baz2 f (Baz v) = Baz <$> f v
baz2 _f s = pure s

这些非常像遍历，但它们肯定不是 lens 意义上的 Traversal。此外，严格来说，它们都不比另一个更通用，包含两者的更灵活的版本看起来不像 Traversal。所以 makeLenses 甚至尝试似乎都不合理。

为什么 makeLenses 不为某些量化的构造函数派生透镜？

Why doesn't makeLenses derive a lens for some quantified constructors?

haskell

gadt

haskell-lens