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

Question

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

谢谢

Answer 1

DataKinds 是一个允许将数据类型提升到类型级别的扩展。这恰恰意味着一堆蠕虫(这是依赖类型的一步)，所以我会尝试将这个解释集中在通用镜头使用它的原因上(但请记住我正在简化在这里)。

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

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