Re: [問題] GADT 概念
板主要我回我只好回了... 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
推
11/30 02:56, , 1F
11/30 02:56, 1F
推
12/05 04:05, , 2F
12/05 04:05, 2F
討論串 (同標題文章)
PLT 近期熱門文章
PTT數位生活區 即時熱門文章
