现实世界中使用GADT的

是否有真实使用广义代数数据类型的任何好的资源?

在哈斯克尔维基给出的例子是太短,给我GADT的现实可能性的洞察力。

谢谢

--------------解决方案-------------

我已经找到了“提示”单子(从“MonadPrompt”包),在几个地方非常有用的工具(以及从“业务”包。结合GADTs(相当于“计划”单子是它打算如何用),它可以让你做嵌入式语言非常便宜,非常灵活,有一个相当不错的文章中的单子阅读器问题15被称为“冒险在三个单子”是有一个很好的介绍提示单子还有一些现实的GADTs 。

GADTs可以给你比普通的ADT强强制类型的保证。 例如,您可以强制二叉树的类型系统级进行平衡,如在此实现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

每个节点都有一个类型编码的深入,所有的叶子所在。 树是那么一个空树,一个单值,或者未指定深度的节点,使用GADTs了。

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

类型系统保证你只有平衡的节点可以构造。 这意味着,实施类似操作时insert这种树,你的代码类型检查,只有当它的结果始终是一个平衡树。

GADTs是感性的家庭从依赖性类型的弱近似语言,所以让我们从这儿开始吧。

电感式家庭是一个依赖性类型语言中的核心数据类型的引入方法。 例如,在阿格达您定义的自然数是这样

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

因此,乍一看,你可能会认为GADTs都干脆利落额外的语法。 这只是冰山的最顶端,但。



阿格达有能力代表各种型号陌生而奇怪的一个Haskell程序员。 一个简单的一种是有限集的类型。 这种类型是这样写Fin 3和表示组数字 {0, 1, 2} 同样地, Fin 5表示组数字{0,1,2,3,4}

这应该是很奇怪的,在这一点上。 首先,我们指的是它有一个普通数字作为“类型”参数的类型。 其次,目前还不清楚这是什么意思为Fin n代表集合{0,1...n} 在现实阿格达我们会做一些更强大,但它足以说,我们可以定义一个contains函数

contains : Nat -> Fin n -> Bool
contains if = ?

现在,这是奇怪的,因为再的“自然”的定义contains会是这样的i < nn是一个值只存在于型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之间有许多差异,但我们可以专注于精确的一个最贴近的理解GADTs。

在GADTs和感性的家庭,你得到一个机会来指定构造函数确切类型。 这可能是无聊

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 (SZ)) -- 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 (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))

但是请注意,我们已经失去了很多的方便了感性的家庭。 例如,我们不能用我们的类型常规数字文字(尽管这在技术上只是一个把戏阿格达反正),我们需要创建一个单独的“类型的NAT”和“价值NAT”,并使用GADT将它们连接在一起,而且我们也会觉得,假以时日,虽然式液位数学是很痛苦的阿格达是可以做到的。 在Haskell这是令人难以置信的痛苦,往往不能。

例如,它可以定义一个weaken的阿格达的概念Fin

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

这里我们提供了一个非常有趣的第一值,一个证明n <= m这使我们能够嵌入“的值小于n到该组“值小于m ”。 我们可以在Haskell做同样的,技术上的,但它需要的类型类序言沉重的滥用。



因此,GADTs是感性的家庭依赖性类型语言是弱,笨拙的相似之处。 为什么我们希望他们在Haskell摆在首位?

基本上,因为不是所有的类型不变量需要感性的家庭的全部力量来表达和GADTs回暖表现,可实施在Haskell,和类型推断之间的特定妥协。

有用的GADTs表达一些例子是不能有红黑财产无效或者干脆类型的演算嵌入高阶像差小猪釜底抽薪Haskell的类型系统红黑树。

在实践中,也经常看到GADTs使用他们的隐性生存环境。 例如,该类型

data Foo where
Bar :: a -> Foo

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

> :t Bar 4 :: Foo

的方式,有时是方便。 如果你仔细看,从维基百科的高阶像差的示例使用此为a type参数App的构造。 为了表达不GADTs这种说法是存在的环境搞得一团糟,但GADT语法使得自然。

我喜欢在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

这是一个简单的答案,不过请查询哈斯克尔维基教科书。 它引导你虽然GADT了良好类型的表达式目录树,这是一个相当典型的例子:http://en.wikibooks.org/wiki/Haskell/GADT

GADTs也用于执行类型相等:http://hackage.haskell.org/package/type-equality。 我找不到正确的纸张引用这个副手 - 这种技术现在做了它的方式顺利进入民间传说。 它是用来相当不错,然而,奥列格的类型无标签的东西。 见,如节类型汇编成GADTs。 http://okmij.org/ftp/tagless-final/#tc-GADT

分类:哈斯克尔 时间:2015-03-15 人气:0
本文关键词: 哈斯克尔,gadt
分享到:

相关文章

Copyright (C) 55228885.com, All Rights Reserved.

55228885 版权所有 京ICP备15002868号

processed in 2.219 (s). 10 q(s)