真實世界中使用GADT

Question

實際使用廣義代數數據類型是否有很好的資源？

haskell wikibook中給出的示例太短，無法讓我深入瞭解GADT的真實可能性。

謝謝

Answer 1

我發現「提示」monad（來自「MonadPrompt」包）是一個非常有用的工具，在幾個地方（以及來自「操作」包的等效「程序」monad）與GADT（這是它使你能夠非常便宜且非常靈活地製作嵌入式語言。在Monad Reader issue 15中有一篇很好的文章叫做「三個Monad中的冒險」，它有一個很好的介紹Prompt monad以及一些現實中的GADTs

Answer 2

這是一個簡短的答案，但請參閱Haskell Wikibook。它會引導您通過一個良好類型的表達式樹的GADT，這是一個相當典型的例子：http://en.wikibooks.org/wiki/Haskell/GADT

GADT也用於實現類型相等：http://hackage.haskell.org/package/type-equality。我無法找到正確的論文供參考 - 現在這種技術已經很好地融入了民間傳說。然而，它在奧列格的無標籤內容中使用得相當好。參見例如有關編入GADT的部分。 http://okmij.org/ftp/tagless-final/#tc-GADT

Answer 3

我喜歡the GHC manual中的例子，它是GADT核心思想的一個快速演示：您可以將正在操作的語言的類型系統嵌入到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。

Answer 4

GADTs可以爲您提供比常規ADT更強大的強制類型擔保。例如，您可以強制二叉樹的2-3 treesthis implementation的類型系統級進行平衡，如：

{-# 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對這些樹木實施操作的時候，你的 代碼類型檢查僅當它的結果總是平衡樹。

Answer 5

GADTs從依賴輸入電感家庭弱近似語言，讓我們開始有代替。

感性的家庭處於依賴性類型語言中的核心數據類型的引入方法。例如，在阿格達您定義的自然數這樣

data Nat : Set where 
    zero : Nat 
    succ : Nat -> Nat 

這是不是很花哨，它本質上是一樣的東西Haskell的定義

data Nat = Zero | Succ Nat 

確實在GADT語法哈斯克爾形式更類似於

{-# LANGUAGE GADTs #-} 

data Nat where 
    Zero :: Nat 
    Succ :: Nat -> Nat 

所以，乍一看你可能會認爲GADTs是乾脆利落額外的語法。這只是冰山一角。

---

Agda有能力代表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 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 

這讓我們看到，有兩個居民，也表明了類型的計算是如何發生的一點點。特別地，zerof類型中的(n : Nat)位反映了實際的值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) 
    ... 

特別是，我們正在濫用修改的能力返回類型基於特定使用的值構造函數。這允許我們將一些價值信息反映到類型中，並生成更精細的指定（纖維）類型。

---

那麼我們可以用他們做什麼？那麼，我們可以用一點肘部潤滑脂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) 

...那麼我們可以利用這些建立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中，這是非常痛苦的，而且往往不能。

例如，它可能在阿格達的Fin類型定義weaken概念

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

，我們提供了一個非常有趣的第一值，證明了n <= m這使我們能夠嵌入「的值小於n」轉換成「小於m」的值。在技​​術上，我們可以在Haskell中做同樣的事情，但它需要嚴重濫用類型序言。

---

因此，GADTs是一種類似於依賴型語言的歸納系列，它們更弱，更笨拙。我們爲什麼首先要在Haskell中使用它們？基本上，因爲並非所有的類型不變式都需要歸納系列的全部功能來表達，並且GADT選擇了表達性，Haskell中的可實現性和類型推斷之間的特定折衷。

有用的GADT表達式的一些示例是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。

實際上，您還經常看到GADT用於其隱式存在上下文。例如，類型

data Foo where 
    Bar :: a -> Foo 

隱式隱藏的方式，有時是方便的使用存在量化

> :t Bar 4 :: Foo 

的a型變量。如果仔細觀察，維基百科的HOAS示例將其用於App構造函數中的a類型參數。爲了在沒有GADT的情況下表達這個陳述將會是一團混亂的存在上下文，但是GADT語法使得它很自然。