45

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

haskell wikibook中给出的示例太短，无法让我深入了解 GADT 的真正可能性。

4

5 回答 5

54

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表示 set意味着什么{0,1...n}。在真正的 Agda 中，我们会做一些更强大的事情，但只要说我们可以定义一个contains函数就足够了

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

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

我们可以通过查看它的定义来检查它是什么Fin赋予了它该属性。

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

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

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

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

是什么提供了这些能力？老实说，依赖类型的归纳系列和常规的 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 (S Z))

*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 中，这是非常痛苦的，而且通常不能。

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

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

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

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

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

有用的 GADT 表达式的一些示例是红黑树，它不能使红黑属性无效或简单类型的 lambda 演算嵌入作为 HOAS 捎带 Haskell 类型系统。

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

data Foo where
  Bar :: a -> Foo

a使用存在量化隐式隐藏类型变量

> :t Bar 4 :: Foo

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

于 2014-01-17T15:31:58.777 回答
26

GADT 可以为您提供比常规 ADT 更强的类型强制保证。例如，您可以强制在类型系统级别上平衡二叉树，就像在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在此类树上实现操作时，您的代码仅在其结果始终是平衡树时才进行类型检查。

于 2013-04-27T11:21:01.007 回答
17

我发现“提示”monad（来自“MonadPrompt”包）在几个地方是一个非常有用的工具（以及来自“操作”包的等效“程序”monad。结合 GADT（这就是它的意图）可以使用），它可以让您非常便宜且非常灵活地制作嵌入式语言。在Monad Reader 第 15 期有一篇很好的文章，名为“Adventures in Three Monads”，很好地介绍了 Prompt monad 以及一些现实的 GADT .

于 2010-10-05T14:45:19.690 回答
4

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

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

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

或者

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

并且定义Term仍然会通过。

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

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

因为我们需要递归调用来eval返回一个Int，而我们又想返回一个Bool。

于 2010-10-08T00:13:51.510 回答
2

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

GADT 也用于实现类型相等：http ://hackage.haskell.org/package/type-equality 。我找不到合适的论文来参考这个副手——这种技术现在已经很好地融入了民间传说。然而，它在 Oleg 的 typedless 东西中使用得很好。参见，例如关于类型化编译成 GADT 的部分。http://okmij.org/ftp/tagless-final/#tc-GADT

于 2010-10-04T23:15:25.130 回答