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

Question

如果我尝试使用通用镜头包中的@符号访问类型的字段，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

换句话说，我们可以让类型级别的程序产生价值级别的结果。这就是通用镜头的用处。此软件包将其用于字段。当您具有以下类型时：

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