板主要我回我只好回了... 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