板主要我回我只好回了... XD ※ 引述《command (ITRS)》之銘言： : 所以說GADT在Haskell上面給我們一種方式去定義generic type可以包含其他的type? 很操作性地舉例，在 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 有它是 較晚近的事情。 : 看到一個寫法, 不知道這樣算不算是dependent type的一種應用XD 其實不太算哩。通常 dependent type 指的是 type 可以 dependent on value, 但在上例中 Expr a 的那個 a 仍必須是 type (Int, Bool...) 不能是 value (5, False ...). : 利用type讓head function不用檢查是不是nil : data Empty : data NonEmpty : data List x y where : Nil :: List a Empty : Cons:: a -> List a b -> List a NonEmpty : safeHead:: List x NonEmpty -> x : safeHead (Cons a b) = a 嗯，這也是一個好例子。事實上若在一個有 dependent type 的 語言裡面，你可以進一步用那個參數表達該 list 的長度: data List a n where Nil :: List a 0 Cons :: a -> List a n -> List a (1+n) 可是在 Haskell 裡面是不能這麼做的。一個模擬的方式是在 type 的層次上定義 0 和 1+. 把 type 和 value 混一起到底好不好，則是目前仍沒有定論的。 --

※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 137.132.201.238