GADT 的实际使用

Question

如何使用广义代数数据类型？

haskell wikibook 中给出的示例太短，无法让我了解真实情况GADT 的可能性。

Answer 1

与常规 ADT 相比，GADT 可以为您提供更强的类型强制保证。例如，您可以强制二叉树在类型系统级别上平衡，如 此实现 2-3 棵树：

{-# LANGUAGE GADTs #-}

data Zero
data Succ s = Succ s

data Node s a where
    Leaf2 :: a -> Node Zero a
    Leaf3 :: a -> a -> Node Zero a
    Node2 :: Node s a -> a -> Node s a -> Node (Succ s) a
    Node3 :: Node s a -> a -> Node s a -> a -> Node s a -> Node (Succ s) a

每个节点都有一个类型编码的深度，其所有叶子都驻留在其中。那么一棵树就是
空树、单例值或未指定深度的节点
使用 GADT。

data BTree a where
    Root0 :: BTree a
    Root1 :: a -> BTree a
    RootN :: Node s a -> BTree a

类型系统保证只能构造平衡节点。
这意味着，当在此类树上实现诸如 insert 之类的操作时，您的
仅当其结果始终是平衡树时，代码才进行类型检查。

Answer 2

我发现“Prompt”monad（来自“MonadPrompt”包）在几个地方都是一个非常有用的工具（以及“Operational”包中的等效“Program”monad）。与 GADT 结合（这就是它的目的）使用），它允许您非常便宜且非常灵活地制作嵌入式语言Monad Reader 第 15 期 称为“三个 Monad 的冒险”，其中对 Prompt monad 以及一些现实的 GADT 进行了很好的介绍。

Answer 3

我喜欢 GHC 中的示例手册。这是 GADT 核心思想的快速演示：您可以将正在操作的语言的类型系统嵌入到 Haskell 的类型系统中。这让你的 Haskell 函数假设并强制它们保留语法树对应于类型良好的程序。

当我们定义Term时，我们选择什么类型并不重要。我们可以写

data Term a where
  ...
  IsZero :: Term Char -> Term Char

or

  ...
  IsZero :: Term a -> Term b

并且 Term 的定义仍然会进行。

只有当我们想要计算Term时，例如在定义eval时，类型才重要。我们需要这样做，

  ...
  IsZero :: Term Int -> Term Bool

因为我们需要递归调用 eval 来返回 Int，并且我们希望依次返回 Bool。

Answer 4

这是一个简短的答案，但请参阅 Haskell Wikibook。它引导您了解类型良好的表达式树的 GADT，这是一个相当规范的示例： http: //en.wikibooks.org/wiki/Haskell/GADT

GADT 也用于实现类型相等： http://hackage.haskell.org/package/type-equality。我找不到合适的论文来参考这一即兴表演——这种技术现在已经深入民间传说。然而，它在 Oleg 的类型化无标签内容中使用得很好。例如，请参阅有关 GADT 类型编译的部分。 http://okmij.org/ftp/tagless-final/#tc-GADT

Answer 5

GADT 是来自依赖类型语言的归纳族的弱近似——所以让我们从这里开始。

归纳族是依赖类型语言中的核心数据类型引入方法。例如，在 Agda 中，您定义这样的自然数，

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat 

这并不是很花哨，它本质上与 Haskell 定义相同

data Nat = Zero | Succ Nat

，而且实际上在 GADT 语法中，Haskell 形式更加相似。

{-# LANGUAGE GADTs #-}

data Nat where
  Zero :: Nat
  Succ :: Nat -> Nat

所以，乍一看，您可能会认为 GADT只是简洁的额外语法。但这只是冰山一角。

---

Agda 能够表示 Haskell 程序员不熟悉和陌生的各种类型。一种简单的类型是有限集类型。此类型的写法类似于Fin 3，代表数字{0, 1, 2}的集合。同样，Fin 5 表示一组数字{0,1,2,3,4}。

在这一点上这应该是很奇怪的。首先，我们指的是一种具有常规数字作为“类型”参数的类型。其次，尚不清楚 Fin n 表示集合 {0,1...n} 的含义。在真正的 Agda 中，我们会做一些更强大的事情，但我们可以定义一个 contains 函数就足够了。

contains : Nat -> Fin n -> Bool
contains i f = ?

现在这又很奇怪，因为 contains 的“自然”定义类似于 i <; n，但是 n 是一个仅存在于 Fin n 类型中的值，我们不应该能够如此轻松地跨越这个鸿沟。虽然事实证明这个定义并不是那么简单，但这正是归纳族在依赖类型语言中所具有的力量——它们引入依赖于它们的类型的值，而类型又依赖于它们的值。

---

我们可以通过查看其定义来检查 Fin 赋予其该属性的内容。

data Fin : Nat -> Set where
  zerof : (n : Nat) -> Fin (succ n)
  succf : (n : Nat) -> (i : Fin n) -> Fin (succ n)

这需要做一些工作才能理解，因此作为示例，让我们尝试构造一个 Fin 2 类型的值。有几种方法可以做到这一点（事实上，我们会发现正好有 2 个）

zerof 1           : Fin 2
zerof 2           : Fin 3 -- nope!
zerof 0           : Fin 1 -- nope!
succf 1 (zerof 0) : Fin 2

这让我们看到有两个居民，并且还演示了类型计算是如何发生的。特别是，zerof 类型中的 (n : Nat) 位反映了实际值 n该类型允许我们为任何 n : Nat 形成 Fin (n+1)。之后，我们重复应用 succf 将 Fin 值增加到正确的类型族索引（索引 Fin 的自然数）。

是什么提供了这些能力？老实说，依赖类型归纳系列和常规 Haskell ADT 之间存在许多差异，但我们可以专注于与理解 GADT 最相关的确切差异。

在 GADT 和归纳族中，您有机会指定构造函数的精确类型。这可能很无聊

data Nat where
  Zero :: Nat
  Succ :: Nat -> Nat

或者，如果我们有更灵活的索引类型，我们可以选择不同的、更有趣的返回类型

data Typed t where
  TyInt  :: Int                -> Typed Int
  TyChar :: Char               -> Typed Char
  TyUnit ::                       Typed ()
  TyProd :: Typed a -> Typed b -> Typed (a, b)
  ...

特别是，我们滥用了根据特定值修改返回类型的能力使用的构造函数。这使我们能够将一些值信息反映到类型中并生成更精细指定（纤维化）的类型。

---

那么我们能用它们做什么呢？好吧，通过一点点苦劳，我们可以 在 Haskell 中生成 Fin。简而言之，它要求我们在类型中定义自然数的概念

data Z
data S a = S a

> undefined :: S (S (S Z))  -- 3

...然后使用 GADT 将值反映到这些类型中......

data Nat where
  Zero :: Nat Z
  Succ :: Nat n -> Nat (S n)

然后我们可以像我们一样使用它们来构建 Fin在 Agda 中...

data Fin n where
  ZeroF :: Nat n -> Fin (S n)
  SuccF :: Nat n -> Fin n -> Fin (S n)

最后，我们可以构造恰好两个 Fin (S (SZ)) 值

*Fin> :t ZeroF (Succ Zero)
ZeroF (Succ Zero) :: Fin (S (S Z))

*Fin> :t SuccF (Succ Zero) (ZeroF Zero)
SuccF (Succ Zero) (ZeroF Zero) :: Fin (S (S Z))

但请注意，我们已经失去了归纳族的很多便利性。例如，我们不能在类型中使用常规数字文字（尽管这在技术上只是 Agda 中的一个技巧），我们需要创建一个单独的“type nat”和“value nat”并使用 GADT 将它们链接在一起，随着时间的推移，我们还会发现，虽然类型级数学在 Agda 中很痛苦，但它是可以完成的。在 Haskell 中，这是非常痛苦的，而且通常不能。

例如，可以在 Agda 的 Fin 类型中定义一个 weaken 概念

weaken : (n <= m) -> Fin n -> Fin m
weaken = ...

，其中我们提供一个非常有趣的第一个值，即 n <= mn <= m code> 允许我们将“小于 n 的值”嵌入到“小于 m 的值”集合中。从技术上讲，我们可以在 Haskell 中做同样的事情，但它需要大量滥用类型类序言。

---

因此，GADT 类似于依赖类型语言中的归纳族，但更弱且更笨拙。为什么我们首先要在 Haskell 中使用它们？

基本上是因为并非所有类型不变量都需要归纳族的全部功能来表达，并且 GADT 在表达性、Haskell 中的可实现性和类型推断之间选择特定的折衷方案。

有用的 GADT 表达式的一些示例是 不能具有红黑关系的红黑树属性无效或嵌入为 HOAS 搭载 Haskell 的简单类型 lambda 演算类型系统。

在实践中，您还经常看到 GADT 用于隐式存在上下文。例如，该类型

data Foo where
  Bar :: a -> Foo

隐式隐藏 a 类型变量

> :t Bar 4 :: Foo

使用存在量化以有时方便的方式 。如果您仔细查看，维基百科中的 HOAS 示例将其用作 App 构造函数中的 a 类型参数。在没有 GADT 的情况下表达该语句将是存在上下文的混乱，但 GADT 语法使其变得自然。