J. *_*son 52
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)
...
特别是,我们滥用基于所使用的特定值构造函数修改返回类型的能力.这允许我们将一些价值信息反映到类型中并产生更精细的(纤维)类型.
那么我们可以用它们做什么呢？好吧,我们可以在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表达式的一些示例是红黑树,其不能使Red-Black属性无效或简单类型的lambda演算嵌入作为HOAS背负Haskell类型系统.
在实践中,您还经常看到GADT用于隐含的存在上下文.例如,类型
data Foo where
Bar :: a -> Foo
隐式隐藏a使用存在量化的类型变量
> :t Bar 4 :: Foo
以某种方式有时方便.如果仔细观察,维基百科的HOAS示例将其用于构造函数中的atype参数App.在没有GADT的情况下表达该陈述将是一堆存在的语境,但GADT语法使其自然.
Pet*_*lák 24
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树的操作时,代码类型只检查其结果是否始终是平衡树.
mok*_*kus 15
我发现"Prompt"monad(来自"MonadPrompt"软件包)在一些地方是一个非常有用的工具(以及来自"操作"软件包的等效"Program"monad.与GADTs结合使用(这是它的意图)使用它,它允许你非常便宜和非常灵活地制作嵌入式语言.在Monad Reader问题15中有一篇非常好的文章,名为"三个Monad中的冒险",它对Prompt monad以及一些现实的GADT进行了很好的介绍. .