GADT的实际应用

Monad Reader issue 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

Agda有能力表示Haskell程序员所不熟悉和陌生的各种类型。一个简单的是有限集的类型。这个 写得像 Fin 3 代表了 数量 {0, 1, 2} . 同样地, Fin 5 表示一组数字 {0,1,2,3,4} .

在这一点上,这应该是相当奇怪的。首先,我们指的是一个类型,它有一个正则数作为“type”参数。第二,不清楚这对我们意味着什么 Fin n 表示集合 {0,1...n} . 在真正的Agda中,我们会做一些更强大的事情,但是我们可以定义一个 contains 功能

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

现在这又奇怪了,因为“自然”的定义 包含 大概是 i < n ,但是 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 反映实际情况 价值 使我们能够形成 Fin (n+1) 对于任何 n : Nat . 在那之后,我们使用 succf 增加我们的 鳍 将值添加到正确的类型族索引中(索引 ).

准确的 构造函数的类型。这可能很无聊

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)
  ...

特别是,我们滥用了基于 特别 使用了值构造函数。这允许我们将一些值信息反映到类型中,并生成更精细的指定(fibered)类型。

那我们能拿他们怎么办?好吧,用一点肘部润滑脂我们就可以了 produce Fin in Haskell

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)

... 然后我们可以用这些来建造 就像我们在阿格达做的那样。。。

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中的类型级数学是痛苦的,但这是可以做到的。在哈斯凯尔这是难以置信的痛苦,往往不能。

例如,可以定义 weaken Agda的概念 类型

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

n <= m 它允许我们嵌入“小于 不 m

因此,gadt类似于依赖类型语言中的归纳族,这些语言较弱且笨拙。我们为什么要把他们放在哈斯克尔?

基本上,因为并非所有类型不变量都需要归纳族的全部表达能力,GADT在Haskell中的表达性、可实现性和类型推断之间选择了一个特殊的折衷。

一些有用的GADTs表达式示例如下 Red-Black Trees which cannot have the Red-Black property invalidated 或 simply-typed lambda calculus embedded as HOAS piggy-backing off the Haskell type system .

data Foo where
  Bar :: a -> Foo

隐式隐藏 a

> :t Bar 4 :: Foo

一 中的类型参数 App

gadt可以提供比常规adt更强大的类型强制保证。例如,可以强制在类型系统级别平衡二叉树,如 this implementation 2-3 trees

{-# 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 在这样的树上,你的 代码类型仅在其结果始终是平衡树时进行检查。

the GHC manual

当我们定义 Term

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

或

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

期限 仍然会通过。

计算 期限 eval ,类型很重要。我们需要

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

评估 返回 Int ,我们想反过来 Bool .

http://en.wikibooks.org/wiki/Haskell/GADT

GADT还用于实现类型相等: http://hackage.haskell.org/package/type-equality . 我找不到合适的论文来参考这种即兴的方法——这种技术已经很好地进入了民间传说。不过,它在Oleg的无标记输入中使用得相当好。例如,请参阅有关将编译键入GADTs的部分。 http://okmij.org/ftp/tagless-final/#tc-GADT