haskell - generic-lens 和 DataKinds GHC 扩展的关系

如果我尝试使用 generic-lens 包中的 @ 符号访问某个类型的字段，GHC 会提示启用 DataKinds 扩展。你能用简单的英语给我解释一下 generic-lens 和 DataKinds 是什么关系吗？

谢谢

最佳答案

DataKinds 是一个扩展，允许将数据类型提升到类型级别。这恰恰意味着是一种蠕虫(这是通往依赖类型的一个步骤)，所以我将尝试将这个解释集中在为什么 generic-lens 使用它上(但请记住，我正在简化这里)。

首先，快速绕道。以下表达式的类型是什么？

mempty

mempty 来自 Monoid 类。然而，与大多数方法相比，它不接受任何参数。那么 Haskell 如何知道将其实例化为哪种类型呢？以下所有情况均属实:

mempty == []
mempty == Sum 0
mempty == Any False

简而言之，Haskell(或 GHC)会推断表达式的类型，并使用该推断来选择正确的实现。有时，推理不起作用。例如，在下面的表达式中:

print mempty

我们必须明确给出类型，如下所示:

print (mempty :: [Int])

@ 符号是一种语法，用于应用通常会推断出的任何类型。所以，在这种情况下，我们可以这样写:

print (mempty @[Int])

不过，它与 :: 不同: @ 符号专门填充了 ghc 试图猜测的第一个类型漏洞。所以我们可以在打印品前面同样应用它:

print @[Int] mempty

因此，您可以看到 @ 是我们将类型应用于表达式的一种方式。然而，它真正让我们做的是从一个类型中获取一个值(很容易)。例如:

{-# LANGUAGE TypeApplications, AllowAmbiguousTypes #-}

class TypeName a where
    name :: String

instance TypeName Int where
    name = "Hello, I'm an Int!"

instance TypeName Bool where
    name = "Bool!"

name @Int

换句话说，我们可以让类型级别的程序产生值级别的结果。这就是 generic-lens 的用武之地。这个包将它用于字段。当您有如下类型时:

data Person
  = Person
  { name :: String
  , age  :: Int
  }

您可以生产两个镜头，一个称为 _name ，另一个称为 _age (或其他)。 generic-lens 做的稍微聪明一点:它有一个函数( fieldLens )，你可以像这样使用:

-- age lens
fieldLens @"age"

最后，这里是我们需要 DataKinds 的地方。传统上来说，在类型级别只允许使用类型，这就是 @ 符号所处理的。不过，上面是一个字符串:解除这个限制正是 DataKinds 所做的。

最后，从技术上讲，您不需要 DataKinds 来伪造上述行为。您可以再次使用类型。事实上，在 DataKinds 之前，人们曾经做过如下事情:

data AgeField = DontConstructMe

fieldLens @AgeField

关于haskell - generic-lens 和 DataKinds GHC 扩展的关系，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/56088579/