※ 引述《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