Re: [問題] GADT 概念

看板PLT (程式語言與理論)作者code17 (None)時間17年前 (2007/12/05 05:04)推噓1(1推 0噓 0→)

留言1則, 1人參與討論串4/6 (看更多)

※ 引述《noctem (noctem)》之銘言： : 板主要我回我只好回了... XD : ※ 引述《command (ITRS)》之銘言： : 很操作性地舉例，在 Haskell 中當我們宣告這樣一個 datatype: : data Foo a = Bar1 a | Bar2 Int Int : 我們得到這兩個 constructors: : Bar1 :: a -> Foo a : Bar2 :: Int -> Int -> Foo a : Generalized algebraic datatype (GADT) 中的那個 "generalized" 指 : 的是 constructor 的結果可以是 Foo a 的 instances, 比如: : data Foo a where : Bar1 :: a -> Foo () : Bar2 :: Int -> Int -> Foo Int : 這個參數 a 有許多用途，大致上說來都是讓 compiler 有多一些 : 資訊可用。比如你舉的例子，讓 parser 表達結果的 type. 在 : Haskell 圈更常見的例子是定義一個表達算式的 datatype, 另外 : 用一個參數註明它 eval 後的型別: : data Expr a where : Num :: Int -> Expr Int : Plus :: Expr Int -> Expr Int -> Expr Int : T :: Expr Bool : ... : 這樣一來我們可以確定不准有 Plus T (Num 3) 這樣的式子。 : GADT 在 dependent type 圈子中出現得更早。 Haskell 有它是 : 較晚近的事情。以前就聽說GADT，但一直只是聽說，也沒去看paper，概念模糊。這裡的解釋很通俗，非常感謝！有幾個概念上的問題想提問： 1) 好像GADT所解決的問題，以前在ML裡一直是用phantom types 來作的，不知道這個理解對不對。當然GADT顯然要干淨得多，不需要定義額外的constructor function也不需要module level的 abstraction。但我想知道這兩種技術在表達能力上一樣強嗎？或是GADT可以表達一些phantom types不能表達的情況？ 2) 如果在ML的類型系統裡加入GADT，type inference依然是 determinic的嗎？ 3) 如果不考慮value-dependent types，而只限於type-dependent types這一範圍，除了GADT還有哪些其他的type arithmetic是可以加到今天的程序語言裡的呢？在這一範圍內，表述能力最強的類型系統是怎樣的呢？謝謝！ -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 64.38.220.185