Haskell/GADT

类型乐趣

多态性
存在量化的类型
高级类型类
幽灵类型
广义代数数据类型 (GADT)
数据类型代数
 类型构造函数和种类

广义代数数据类型，或简称为 GADT，是您熟悉的代数数据类型的推广。基本上，它们允许您明确写下构造函数的类型。在本章中，您将学习为什么这很有用以及如何声明您自己的 GADT。

我们从构建一个简单的嵌入式领域特定语言 (EDSL) 的例子开始，该语言用于简单的算术表达式，它可以通过 GADT 更稳固地构建。接下来是 GADT 语法概述，以及更简单的说明，以及不同的应用来构建安全列表类型，其中 head [] 的等效操作无法进行类型检查，因此不会出现通常的运行时错误：*** Exception: Prelude.head: empty list。

理解 GADT

那么，什么是 GADT 以及它们有什么用？GADT 主要用于实现领域特定语言，因此本节将通过相应的例子来介绍它们。

算术表达式

让我们考虑一个用于算术表达式的简单语言，它由以下数据类型给出

data Expr = I Int         -- integer constants
          | Add Expr Expr -- add two expressions
          | Mul Expr Expr -- multiply two expressions

换句话说，该数据类型对应于抽象语法树，类似于 (5+1)*7 这样的算术项将表示为 (I 5 `Add` I 1) `Mul` I 7 :: Expr。

给定抽象语法树，我们希望对其做些什么；我们希望编译它，优化它等等。首先，让我们编写一个评估函数，它接受一个表达式并计算它所表示的整数值。定义很简单

eval :: Expr -> Int
eval (I n)       = n
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2

扩展语言

现在，假设我们希望将我们的语言扩展为除了整数之外的其他类型。例如，假设我们希望表示相等性测试，因此我们也需要布尔值。我们扩展了 Expr 类型，使其变为

data Expr = I Int
          | B Bool           -- boolean constants
          | Add Expr Expr
          | Mul Expr Expr
          | Eq  Expr Expr    -- equality test

项 5+1 == 7 将表示为 (I 5 `Add` I 1) `Eq` I 7。

与之前一样，我们希望编写一个函数 eval 来评估表达式。但是这次，表达式现在可以表示整数或布尔值，我们必须在返回类型中捕获这一点

eval :: Expr -> Either Int Bool

前两种情况很简单

eval (I n) = Left n
eval (B b) = Right b

但是现在我们遇到了麻烦。我们希望编写

eval (Add e1 e2) = eval e1 + eval e2  -- ???

但这无法进行类型检查：加法函数 + 期望两个整型参数，但 eval e1 的类型为 Either Int Bool，我们需要从中提取 Int。

更糟糕的是，如果 e1 实际上表示一个布尔值 会怎样？以下是一个有效的表达式

B True `Add` I 5 :: Expr

但很明显，它没有意义；我们不能将布尔值加到整数！换句话说，评估可能会返回整数或布尔值，但也可能失败，因为表达式没有意义。我们必须将这一点纳入返回类型

eval :: Expr -> Maybe (Either Int Bool)

现在，我们可以很好地编写这个函数，但这仍然不令人满意，因为我们真正想要做的是让 Haskell 的类型系统排除任何无效表达式；我们不想在解构抽象语法树时自己检查类型。

练习：尽管有我们的目标，但实现 eval 函数可能仍然具有指导意义；请执行此操作。

起点

data Expr = I Int
        | B Bool           -- boolean constants
        | Add Expr Expr
        | Mul Expr Expr
        | Eq  Expr Expr    -- equality test

eval :: Expr -> Maybe (Either Int Bool)
-- Your implementation here.

幽灵类型

所谓的幽灵类型是我们目标的第一步。这种技术是为 Expr 添加一个类型变量，使其变为

data Expr a = I Int
            | B Bool
            | Add (Expr a) (Expr a)
            | Mul (Expr a) (Expr a)
            | Eq  (Expr a) (Expr a)

注意，表达式 Expr a 根本不包含值 a；这就是为什么 a 被称为幽灵类型，它只是一个虚拟变量。将其与列表 [a] 相比较，列表 [a] 确实包含一堆 a。

关键思想是我们将使用 a 来跟踪表达式的类型。而不是让构造函数

Add :: Expr a -> Expr a -> Expr a

可供我们小型语言的用户使用，我们将只提供一个类型更受限制的智能构造函数

add :: Expr Int -> Expr Int -> Expr Int
add = Add

实现方式相同，但类型不同。对其他构造函数也这样做，

i :: Int  -> Expr Int
i = I
b :: Bool -> Expr Bool
b = B

之前有问题的表达式

b True `add` i 5

不再进行类型检查！毕竟，第一个参数的类型为 Expr Bool，而 add 期望一个 Expr Int。换句话说，幽灵类型 a 标记了表达式的预期类型。通过只导出智能构造函数，用户无法创建类型不正确的表达式。

与之前一样，我们希望实现一个评估函数。使用我们新的标记 a，我们可能希望赋予它以下类型

eval :: Expr a -> a

并像这样实现第一个案例。

eval (I n) = n

但遗憾的是，这行不通：编译器如何知道遇到构造函数I意味着a = Int？当然，对于用户在我们的语言中创建的所有表达式来说，情况将如此，因为他们只被允许使用智能构造函数。但从内部来说，像

I 5 :: Expr String

这样的表达式仍然是有效的。事实上，正如你所看到的，a甚至不必是Int或Bool，它可以是任何东西。

我们需要一种方法来限制构造函数本身的返回类型，而这正是泛型数据类型所做的事情。

GADTs

要启用此语言特性，请在文件开头添加{-# LANGUAGE GADTs #-}。

限制构造函数类型的明显表示法是写下它的类型，而这正是 GADTs 的定义方式。

data Expr a where
    I   :: Int  -> Expr Int
    B   :: Bool -> Expr Bool
    Add :: Expr Int -> Expr Int -> Expr Int
    Mul :: Expr Int -> Expr Int -> Expr Int
    Eq  :: Eq a => Expr a -> Expr a -> Expr Bool

换句话说，我们只需列出所有构造函数的类型签名。特别是，标记类型a根据我们的需要专门化为Int或Bool，就像我们对智能构造函数所做的那样。

而 GADTs 的伟大之处在于我们现在可以实现一个利用类型标记的评估函数。

eval :: Expr a -> a
eval (I n) = n
eval (B b) = b
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq  e1 e2) = eval e1 == eval e2

特别是在第一个案例中

eval (I n) = n

编译器现在能够推断出当我们遇到构造函数I时a=Int，并且返回n :: Int是合法的；其他案例也是如此。

总而言之，GADTs 允许我们限制构造函数的返回类型，从而使我们能够利用 Haskell 的类型系统来实现我们的领域特定语言。因此，我们可以实现更多的语言，并且它们的实现变得更简单。

摘要

语法

以下是关于声明 GADTs 语法的快速摘要。

首先，考虑以下普通代数数据类型：熟悉的List和Maybe类型，以及一个简单的树类型RoseTree。

Maybe	List	Rose Tree
data Maybe a = Nothing \| Just a	data List a = Nil \| Cons a (List a)	data RoseTree a = RoseTree a [RoseTree a]

请记住，这些声明引入的构造函数既可以用于模式匹配来解构值，也可以用作函数来构建值。（Nothing和Nil是具有“零个参数”的函数。）我们可以问一下后者是什么类型。

Maybe	List	Rose Tree
> :t Nothing Nothing :: Maybe a > :t Just Just :: a -> Maybe a	> :t Nil Nil :: List a > :t Cons Cons :: a -> List a -> List a	> :t RoseTree RoseTree :: a -> [RoseTree a] -> RoseTree a

很明显，关于Maybe、List和RoseTree构造函数的类型信息等同于我们在最初声明数据类型时提供给编译器的信息。换句话说，也可以通过简单地列出所有构造函数的类型来声明数据类型，而这正是 GADT 语法所做的。

Maybe	List	Rose Tree
data Maybe a where Nothing :: Maybe a Just :: a -> Maybe a	data List a where Nil :: List a Cons :: a -> List a -> List a	data RoseTree a where RoseTree :: a -> [RoseTree a] -> RoseTree a

此语法可以通过语言选项{-#LANGUAGE GADTs #-}使用。它应该很熟悉你，因为它与类型类声明的语法非常相似。如果你习惯于将构造函数视为函数，那么它也很容易记住。每个构造函数都由一个类型签名定义。

新可能性

请注意，当我们询问GHCi关于Nothing和Just的类型时，它返回了Maybe a和a -> Maybe a作为类型。在这些情况下以及其他情况下，与构造函数相关的函数的最终输出类型是我们最初定义的类型 - Maybe a、List a或RoseTree a。总的来说，在标准 Haskell 中，Foo a的构造函数函数具有Foo a作为它们的最终返回类型。如果新语法与旧语法严格等效，那么我们必须对它的使用进行此限制以进行有效的类型声明。

那么 GADTs 为我们添加了什么？能够精确控制你返回的Foo类型。使用 GADTs，Foo a的构造函数不必返回Foo a；它可以返回你能想到的任何Foo blah。例如，在下面的代码示例中，MkTrueGadtFoo构造函数返回一个TrueGadtFoo Int，即使它是针对类型TrueGadtFoo a的。

示例：GADT 让你有更多控制权

data FooInGadtClothing a where
 MkFooInGadtClothing :: a -> FooInGadtClothing a

--which is no different from:  data Haskell98Foo a = MkHaskell98Foo a ,

--by contrast, consider:
 
data TrueGadtFoo a where
  MkTrueGadtFoo :: a -> TrueGadtFoo Int

--This has no Haskell 98 equivalent.

但请注意，你只能进行如此远的泛化...如果你要声明的数据类型是Foo，那么构造函数函数必须返回某种Foo。返回任何其他东西根本行不通。

示例：试试这个。它行不通

data Bar where
  BarNone :: Bar -- This is ok

data Foo where
  MkFoo :: Bar Int-- This will not typecheck

示例

安全的列表

先决条件：我们假设在本节中你了解列表在函数式语言中是如何表示的

注意：本节中的示例还要求启用扩展名 EmptyDataDecls 和 KindSignatures

我们现在已经了解了 GADT 语法赋予我们的额外控制权。唯一的新事物是你可以精确控制返回的数据结构类型。现在，我们能用它来做什么呢？考虑一下简单的 Haskell 列表。当你调用head []时会发生什么？Haskell 会崩溃。你是否曾经希望有一个神奇的head版本，它只接受至少包含一个元素的列表，在这些列表上它永远不会崩溃？

首先，让我们定义一个新类型SafeList x y。我们的想法是拥有类似于普通 Haskell 列表[x]的东西，但在类型中包含一些额外的信息。此额外信息（类型变量y）告诉我们列表是否为空。空列表表示为SafeList x Empty，而非空列表表示为SafeList x NonEmpty。

-- we have to define these types
data Empty
data NonEmpty

-- the idea is that you can have either 
--    SafeList a Empty
-- or SafeList a NonEmpty
data SafeList a b where
-- to be implemented

由于我们有此额外信息，我们现在可以仅对非空列表定义一个函数safeHead！在空列表上调用safeHead将简单地拒绝类型检查。

safeHead :: SafeList a NonEmpty -> a

那么既然我们知道我们想要什么，即safeHead，我们如何实际获得它呢？答案是 GADT。关键是我们利用 GADT 特性返回两种不同的a类型列表，对于Nil构造函数，返回SafeList a Empty，而对于Cons构造函数，则返回SafeList a NonEmpty。

data SafeList a b where
  Nil  :: SafeList a Empty
  Cons :: a -> SafeList a b -> SafeList a NonEmpty

如果没有 GADT，这是不可能的，因为我们所有的构造函数都必须返回相同类型的列表；而使用 GADT，我们现在可以使用不同的构造函数返回不同类型的列表。无论如何，让我们将所有这些内容整合在一起，以及SafeHead的实际定义。

示例：通过 GADT 实现安全的列表

{-#LANGUAGE GADTs, EmptyDataDecls #-}
-- (the EmptyDataDecls pragma must also appear at the very top of the module,
-- in order to allow the Empty and NonEmpty datatype declarations.)

data Empty
data NonEmpty

data SafeList a b where
     Nil :: SafeList a Empty
     Cons:: a -> SafeList a b -> SafeList a NonEmpty

safeHead :: SafeList a NonEmpty -> a
safeHead (Cons x _) = x

将此列表复制到一个文件中，并在ghci -fglasgow-exts中加载。你应该注意到以下区别，分别在非空列表和空列表上调用safeHead。

示例：safeHead是...安全的

Prelude Main> safeHead (Cons "hi" Nil)
"hi"
Prelude Main> safeHead Nil

<interactive>:1:9:
    Couldn't match `NonEmpty' against `Empty'
      Expected type: SafeList a NonEmpty
      Inferred type: SafeList a Empty
    In the first argument of `safeHead', namely `Nil'
    In the definition of `it': it = safeHead Nil

这个抱怨是件好事：这意味着我们现在可以在编译时确保是否在适当的列表上调用safeHead。但是，这也为潜在的风险设置了一个陷阱。考虑以下函数。你认为它的类型是什么？

示例：GADTs 的问题

silly False = Nil
silly True  = Cons () Nil

现在尝试在 GHCi 中加载该示例。你会注意到以下抱怨。

示例：GADTs 的问题 - 抱怨

Couldn't match `Empty' against `NonEmpty'
     Expected type: SafeList () Empty
     Inferred type: SafeList () NonEmpty
   In the application `Cons () Nil'
   In the definition of `silly': silly True = Cons () Nil

silly定义中的案例评估为不同类型的标记列表，导致类型错误。通过 GADT 强加的额外约束，函数无法同时生成空列表和非空列表。

如果我们真的想定义silly，我们可以通过放松Cons的类型来实现，以便它可以构建安全的列表和不安全的列表。

示例：另一种方法

{-#LANGUAGE GADTs, EmptyDataDecls, KindSignatures #-}
-- here we add the KindSignatures pragma,
-- which makes the GADT declaration a bit more elegant.

-- Note the subtle yet revealing change in the phantom type names.
data NotSafe
data Safe


data MarkedList             ::  * -> * -> * where
  Nil                       ::  MarkedList t NotSafe
  Cons                      ::  a -> MarkedList a b -> MarkedList a c


safeHead                    ::  MarkedList a Safe -> a
safeHead (Cons x _)          =  x

-- This function will never produce anything that can be consumed by safeHead,
-- no matter that the resulting list is not necessarily empty.
silly                       :: Bool -> MarkedList () NotSafe
silly False                  =  Nil
silly True                   =  Cons () Nil

上面的修复有一个代价：通过放松Cons的约束，我们放弃了它无法生成空列表的知识。根据我们最初版本的安全列表，例如，我们可以定义一个函数，它接受一个SafeList a Empty参数，并确保Cons产生的任何东西都不会被它接受。对于类似的MarkedList a NotSafe，情况并非如此；可以说，该类型正是因为它限制性较小而用途较小。虽然在这个例子中，问题可能看起来很小，因为空列表的作用不大，但总的来说，值得考虑。

练习
你能实现一个`safeTail`函数吗？这里介绍的两个版本都可以作为有效的起点，以及其他类似的变体。

一个简单的表达式求值器

插入 Wobbly Types 论文中使用的示例...我认为这很有教学意义。

本教程的第一部分已经涵盖了这一点。

讨论

更多示例、思考

我依稀记得在 2006 年的 FOSDEM 上，GADT 与以下内容之间存在某种关系...什么？

幽灵类型

请参阅幻影类型。

存在类型

如果你喜欢存在量化的类型，你可能想注意到它们现在被 GADT 包含了。正如 GHC 手册所说，以下两个类型声明给你同样的东西。

data TE a = forall b. MkTE b (b->a)
data TG a where { MkTG :: b -> (b->a) -> TG a }

见证类型

GADT

练习解答

类型乐趣

多态性 >> 存在量化的类型 >> 高级类型类 >> 幻影类型 >> 广义代数数据类型 (GADT) >> 数据类型代数 >> 类型构造函数 & 种类

编辑本章

Haskell

Haskell 基础 >> 基础 Haskell >> 中级 Haskell >> 单子
 高级 Haskell >> 类型玩乐 >> 更广阔的理论 >> Haskell 性能

库参考 >> 通用实践 >> 专门任务

编辑书籍结构