•  27-09-2019
  •  | 
  •  

题

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

中给出的例子 哈斯克尔维基百科 篇幅太短，无法让我深入了解 GADT 的真正可能性。

有帮助吗？

解决方案

我已经找到了“提示”单子（从“MonadPrompt”包）的若干位置中的非常有用的工具（与来自“业务”包。与GADTs组合（相当于“程序”单子沿其是如何旨在使用），它可以让你做嵌入式语言非常便宜，非常灵活。有一个在的单子读者问题15 所谓的‘在有一个很好的介绍提示单子一些现实GADTs沿着三个单子’的冒险。

其他提示

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

这让我们看到有两个居民，并且还演示了类型计算是如何发生的。特别是， (n : Nat) 位类型为 zerof 反映实际情况 价值 n 进入允许我们形成的类型 Fin (n+1) 对于任何 n : Nat. 。之后我们重复应用 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)
  ...

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

那么我们能用它们做什么呢？好吧，只要一点点苦劳，我们就可以 生产 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 就像我们在阿格达所做的那样......

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 中的一个技巧），我们需要创建一个单独的“类型 nat”和“值 nat”，并使用 GADT 将它们链接在一起，随着时间的推移，我们还会发现，虽然类型级数学在 Agda 中很痛苦，但它是可以完成的。在 Haskell 中，这是非常痛苦的，而且通常不能。

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

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

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

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

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

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

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

data Foo where
  Bar :: a -> Foo

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

> :t Bar 4 :: Foo

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

与常规 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

每个节点都有一个类型编码的深度，其所有叶子都驻留在其中。然后，再次使用GADTS再次使用树，是一个空的树，单例值或一个未指定深度的节点。

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

类型系统保证只能构造平衡节点。这意味着当执行像这样的操作时 insert 在这样的树上，您的代码类型检查只有其结果始终是平衡的树。

我喜欢这个例子 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.

这是一个简单的答案，但查阅Haskell的维基教科书。它引导你虽然GADT了良好的输入表达式树，这是一个相当典型的例子： HTTP： //en.wikibooks.org/wiki/Haskell/GADT

GADTs也用于执行类型相等： http://hackage.haskell.org/package /类型平等。我找不到合适的纸张为这个副手参考 - 这项技术已经通过现在的方式顺利进入民间传说。它是用来相当不错，然而，在奥列格的类型化的无代码的东西。见，例如上键入汇编成一节GADTs。 http://okmij.org/ftp/tagless-final/#tc-GADT

不隶属于 StackOverflow
scroll top