真实世界使用GADT
广义代数数据types的实际应用是否有很好的资源？
在haskell wikibook中给出的例子太短，不能让我了解GADT的真正可能性。
谢谢
我发现“Prompt”Monad（来自“MonadPrompt”包）是一个非常有用的工具，在几个地方（以及来自“operational”包的等效“Program”monad）结合GADT（它是如何打算的它可以让你非常便宜和非常灵活地制作embedded式语言，在Monad Reader第15期的一篇名为“Three Monads Adventures”的文章中有一篇很好的文章，对Prompt monad和一些现实的GADT做了很好的介绍。
GADT是依赖types语言的归纳系统的弱近似 – 所以我们先从那里开始。
诱导族是依赖型语言中的核心数据types引入方法。 例如，在Agda中，你可以像这样定义自然数
data Nat : Set where zero : Nat succ : Nat -> Nat 这不是很花哨，它本质上和Haskell定义一样
data Nat = Zero | Succ Nat
实际上在GADT语法中，Haskellforms更加相似
{-# LANGUAGE GADTs #-} data Nat where Zero :: Nat Succ :: Nat -> Nat
所以，乍一看，你可能会认为GADT只是一些额外的语法。 这只是冰山一angular。
Agda有能力代表Haskell程序员不熟悉和陌生的各种types。 一个简单的是有限集合的types。 这种types写为Fin 3 ，表示数字集合 {0, 1, 2} 。 同样， Fin 5表示一组数字{0,1,2,3,4} 。
这一点应该是相当奇怪的。 首先，我们指的是具有常规数字的types作为“types”参数。 其次， Fin n代表集合{0,1...n}含义并不清楚。 在真正的阿格达我们会做更强大的东西，但是我们可以定义一个contains函数就足够了
contains : Nat -> Fin n -> Bool contains if = ?
现在这又奇怪了，因为contains的“自然”定义是类似于i < n ，但是n是一个只存在于typesFin n中的值，所以我们不应该如此轻易地跨越这个鸿沟。 事实certificate，这个定义并不是那么直截了当，这正是归属家族在依赖types语言中所具有的力量 – 它们引入了取决于其types和types的取决于其价值的价值观。
我们可以通过观察它的定义来研究Fin给它的财产是什么。
data Fin : Nat -> Set where zerof : (n : Nat) -> Fin (succ n) succf : (n : Nat) -> (i : Fin n) -> Fin (succ n)
这需要一点工作来理解，所以作为一个例子，我们可以尝试构build一个Fin 2types的值。 有几种方法可以做到这一点（事实上，我们会发现有2个）
zerof 1 : Fin 2 zerof 2 : Fin 3 -- nope! zerof 0 : Fin 1 -- nope! succf 1 (zerof 0) : Fin 2
这让我们看到有两个居民，也演示了一些types计算是如何发生的。 特别地， zeroftypes的(n : Nat)位将实际值 n反映到允许我们为任何n : Nat形成Fin (n+1)的types中。 之后，我们使用succf重复应用程序将我们的Fin值succf正确的types族索引（索引Fin自然数）。
什么提供这些能力？ 老实说，在一个依赖types的归纳家族和一个常规的Haskell ADT之间有很多不同之处，但是我们可以把精力集中在与理解GADT最相关的东西上。
在GADT和归纳系列中，您有机会指定构造函数的确切types。 这可能是无聊的
data Nat where Zero :: Nat Succ :: Nat -> Nat
或者，如果我们有一个更灵活的索引types，我们可以select不同的，更有趣的返回types
data Typed t where TyInt :: Int -> Typed Int TyChar :: Char -> Typed Char TyUnit :: Typed () TyProd :: Typed a -> Typed b -> Typed (a, b) ...
特别是，我们正在滥用修改返回types的能力，这取决于所使用的特定的值构造函数。 这使我们能够将一些价值信息反映到这种types中，并产生更精细的指定（纤维）types。
那么我们可以用他们做什么？ 那么，用一点点的润滑脂就可以在Haskell生产Fin 。 简而言之，它要求我们定义一种types的自然概念
data Z data S a = S a > undefined :: S (S (SZ)) -- 3
然后GADT将价值反映到这些types中
data Nat where Zero :: Nat Z Succ :: Nat n -> Nat (S n)
那么我们可以用这些来build立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 (SZ)) *Fin> :t SuccF (Succ Zero) (ZeroF Zero) SuccF (Succ Zero) (ZeroF Zero) :: Fin (S (SZ))
但是请注意，我们已经失去了许多诱导家庭的便利。 例如，我们不能在我们的types中使用常规的数字文字（尽pipe这在技术上只是Agda的一个技巧），我们需要创build一个单独的“nattypes”和“值nat”，并使用GADT将它们连接在一起，而且我们还会发现，尽pipe在Agda中，types级math是痛苦的，但是可以完成。 在Haskell这是非常痛苦的，往往不能。
例如，可以在Agda的Fintypes中定义一个weaken概念
weaken : (n <= m) -> Fin n -> Fin m weaken = ...
在那里我们提供了一个非常有趣的第一个值，一个certificaten <= m ，它允许我们将“小于n的值”embedded到“小于m值”的集合中。 在技术上，我们可以在Haskell中做同样的事情，但是它需要大量滥用types序言。
因此，GADT是依赖types语言的归纳系列的相似之处，它们更弱，更笨拙。 为什么我们希望他们在Haskell首先？
基本上，因为并非所有的types不variables都需要归纳系列的全部function来expression，GADT在Haskell中的expression性，可执行性和types推理之间select了一种特殊的折衷scheme。
有用的GADTexpression式的一些例子是Red-Black Trees，它们不能将Red-Black属性无效化或简单types的lambda微积分作为HOAS捎带closuresHaskelltypes系统embedded 。
在实践中，你也经常看到GADT用于它们隐含的存在上下文。 例如，types
data Foo where Bar :: a -> Foo
隐式地使用存在量化来隐藏atypesvariables
> :t Bar 4 :: Foo
以一种有时方便的方式。 如果仔细观察，来自维基百科的HOAS示例将其用于App构造函数中的types参数。 为了expression这种没有GADT的陈述将会是一堆混乱的存在上下文，但是GADT语法使得它很自然。
GADT可以为您提供比常规ADT更强大的强制担保types。 例如，可以强制二叉树在types系统级别上平衡，就像在2-3树的 实现中一样：
{-# LANGUAGE GADTs #-} data Zero data Succ s = Succ s data Node sa where Leaf2 :: a -> Node Zero a Leaf3 :: a -> a -> Node Zero a Node2 :: Node sa -> a -> Node sa -> Node (Succ s) a Node3 :: Node sa -> a -> Node sa -> a -> Node sa -> Node (Succ s) a
每个节点都有其所有叶子所在的types编码的深度。 一棵树就是一棵空树，一个单独值，或一个未指定深度的节点，再次使用GADT。
data BTree a where Root0 :: BTree a Root1 :: a -> BTree a RootN :: Node sa -> BTree a
types系统保证您只能构build平衡的节点。 这意味着在执行像在这样的树上insert操作时，您的代码types只会检查其结果始终是否是平衡树。
我喜欢GHC手册中的例子。 这是一个核心GADT思想的快速演示：您可以将正在操作的语言的types系统embedded到Haskell的types系统中。 这可以让你的Haskell函数承担，并强制他们保留，语法树对应于良好types的程序。
当我们定义Term ，我们select什么types并不重要。 我们可以写
data Term a where ... IsZero :: Term Char -> Term Char
要么
... IsZero :: Term a -> Term b
而Term的定义仍然会经过。
只有一次我们想要在 Term 上进行计算 ，比如在定义eval ，types很重要。 我们需要有
... IsZero :: Term Int -> Term Bool
因为我们需要recursion调用eval来返回一个Int ，而我们又想返回一个Bool 。
这是一个简短的答案，但请参阅Haskell Wikibook。 它引导你通过一个良好types的expression式树GADT，这是一个相当规范的例子： http : //en.wikibooks.org/wiki/Haskell/GADT
GADT也用于实现types相等： http ://hackage.haskell.org/package/type-equality。 我无法find正确的文件来引用这个 – 这种技术现在已经很好地进入了民间传说。 然而，在奥列格的无标签的东西中使用得相当好。 参见例如有关编入GADT的部分。 http://okmij.org/ftp/tagless-final/#tc-GADT
