通用镜头和DataKinds GHC扩展之间的关系

Question

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

- Dragno

Answer 1

DataKinds是一种扩展功能，允许数据类型提升为类型级别。这确切意味着什么有点棘手（这是依赖类型的一步），因此我将尝试将解释集中在为什么generic-lens使用它上面（但请记住我在这里是简化了的）。

首先，简单地说一下。以下表达式的类型是什么？

mempty

mempty来自于Monoid类。然而，与大多数方法相反，它不需要任何参数。那么Haskell如何知道要实例化哪种类型呢？以下所有的陈述都是真实的：

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

简而言之，Haskell (或者说 GHC) 会 推断 表达式的类型，并使用推断结果来选择正确的实现方案。有时，推断会失败。例如，在以下表达式中：

print mempty

我们需要明确地指定类型，像这样：

print (mempty :: [Int])

< p > @ 符号是应用通常会被推断的任何类型的语法。因此，在这种情况下，我们可以写成：

print (mempty @[Int])

然而，@符号与::并不相同：@符号专门填补了ghc试图猜测的第一个类型漏洞。因此，我们在print前面同样可以使用它：

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

- oisdk