Re: [問題] GADT 概念

看板PLT (程式語言與理論)作者noctem (noctem)時間17年前 (2007/12/06 11:21)推噓2(2推 0噓 1→)

留言3則, 2人參與討論串5/6 (看更多)

哇，高手來了。都是很有意思而且不很容易答的問題哩。 :) ※ 引述《code17 (None)》之銘言： : 1) 好像GADT所解決的問題，以前在ML裡一直是用phantom types : 來作的，不知道這個理解對不對。當然GADT顯然要干淨得多，不需 : 要定義額外的constructor function也不需要module level的 : abstraction。但我想知道這兩種技術在表達能力上一樣強嗎？或 : 是GADT可以表達一些phantom types不能表達的情況？先確認一下我們說的 phantom type 是什麼。我所知道的第一種是來自Leijen & Meijer: http://www.usenix.org/events/dsl99/full_papers/leijen/leijen.pdf 之所以叫做 phantom type 是因為右手邊有個沒出現在左邊的 type variable, 如: data Expr a = Expr PrimExpr -- 沒有 a data PrimExpr = ... -- 真正的資料結構定義這個 a 可以存放一些資訊。例如，如果我們只准許用幾個定好的 method 來產生 Expr: plus :: Expr Int -> Expr Int -> Expr Int and :: Expr Bool -> Expr Bool -> Expr Bool 我們就可以確保算式的 type 是對的。這樣的 phantom type 似乎在跨模組界限時會出現一些問題，所以 Cheney & Hinze 等人另外提了一種 "First-class phantom type", 大致上的主意是用一些資料結構來確保 type equality （後述）。在我理解中，first-class phantom type 只要再加上一些語法修飾就是 GADT 了。 http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf http://ecommons.library.cornell.edu/handle/1813/5614 Cheney & Hinze 談到用 2nd-rank polymorphism 就可以模擬 GADT. 例如下面這個宣告: data Expr a where ... Num :: Int -> Expr Int 其實可以 encode 成: data Expr a = Num :: (a :=: Int) -> Int -> Expr a 其中 (a :=: Int) 是某個資料結構，強迫 a 會等於 Int. 這種資料結構可以這樣做: data a :=: b = Proof (forall a . f a -> f b) 兩個 type a 和 b 一樣，如果他們在任何 context f 之下都一樣。唯一有這個 type: forall a . f a -> f b 的 term 是 id, 所以 a 和 b 非得是一樣的 type 不可。 refl :: a :=: a refl = Proof id 這表示 algebraic data type 再加上 2nd-rank polymorphism 就可以模擬 GADT. : 2) 如果在ML的類型系統裡加入GADT，type inference依然是 : determinic的嗎？據我所知並不是的。原因之一是有了 GADT 也該有 polymorphic recursion（例如傳回 Bool 的 eval 可能會去 call 傳回 Int 的 eval），但 polymorphic recursion 的 type inference （若沒有 type annotation）本來就是 undecidable 的。關於 GADT 的 type inference 可以參考 http://research.microsoft.com/Users/simonpj/papers/gadt/index.htm : 3) 如果不考慮value-dependent types，而只限於type-dependent : types這一範圍，除了GADT還有哪些其他的type arithmetic是可以 : 加到今天的程序語言裡的呢？在這一範圍內，表述能力最強的類型系統 : 是怎樣的呢？ Hmmm... 我只知道在以前用 Haskell 的 type class 也可以做一些 type arithmetic (我玩過一點點，但實在是太辛苦了...). 而既然 type class 可以，用 ML 的 module 應該也是可以的。是否還有其他的方式，以及他們的 expressiveness 方面我就不是很清楚了。你知道其他的嗎？ :) -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 140.109.20.217