哇，高手来了。都是很有意思而且不很容易答的问题哩。 :) ※ 引述《code17 (None)》之铭言： : 1) 好像GADT所解决的问题，以前在ML里一直是用phantom types : 来作的，不知道这个理解对不对。当然GADT显然要干净得多，不需 : 要定义额外的constructor function也不需要module level的 : abstraction。但我想知道这两种技术在表达能力上一样强吗？或 : 是GADT可以表达一些phantom types不能表达的情况？ 先确认一下我们说的 phantom type 是什麽。我所知道的第一种 是来自Leijen & Meijer: http://www.usenix.org/events/dsl99/full_papers/leijen/leijen.pdf 之所以叫做 phantom type 是因为右手边有个没出现在左边的 type variable, 如: data Expr a = Expr PrimExpr -- 没有 a data PrimExpr = ... -- 真正的资料结构定义 这个 a 可以存放一些资讯。例如，如果我们只准许用几个定好的 method 来产生 Expr: plus :: Expr Int -> Expr Int -> Expr Int and :: Expr Bool -> Expr Bool -> Expr Bool 我们就可以确保算式的 type 是对的。 这样的 phantom type 似乎在跨模组界限时会出现一些问题，所以 Cheney & Hinze 等人另外提了一种 "First-class phantom type", 大致上的主意是用一些资料结构来确保 type equality （後述）。 在我理解中，first-class phantom type 只要再加上一些语法修饰 就是 GADT 了。 http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf http://ecommons.library.cornell.edu/handle/1813/5614 Cheney & Hinze 谈到用 2nd-rank polymorphism 就可以模拟 GADT. 例如下面这个宣告: data Expr a where ... Num :: Int -> Expr Int 其实可以 encode 成: data Expr a = Num :: (a :=: Int) -> Int -> Expr a 其中 (a :=: Int) 是某个资料结构，强迫 a 会等於 Int. 这种资料结构可以这样做: data a :=: b = Proof (forall a . f a -> f b) 两个 type a 和 b 一样，如果他们在任何 context f 之下都 一样。唯一有这个 type: forall a . f a -> f b 的 term 是 id, 所以 a 和 b 非得是一样的 type 不可。 refl :: a :=: a refl = Proof id 这表示 algebraic data type 再加上 2nd-rank polymorphism 就可以模拟 GADT. : 2) 如果在ML的类型系统里加入GADT，type inference依然是 : determinic的吗？ 据我所知并不是的。原因之一是有了 GADT 也该有 polymorphic recursion（例如传回 Bool 的 eval 可能会去 call 传回 Int 的 eval），但 polymorphic recursion 的 type inference （若没有 type annotation）本来就是 undecidable 的。 关於 GADT 的 type inference 可以参考 http://research.microsoft.com/Users/simonpj/papers/gadt/index.htm : 3) 如果不考虑value-dependent types，而只限於type-dependent : types这一范围， 除了GADT还有哪些其他的type arithmetic是可以 : 加到今天的程序语言里的呢？ 在这一范围内，表述能力最强的类型系统 : 是怎样的呢？ Hmmm... 我只知道在以前用 Haskell 的 type class 也可以做一些 type arithmetic (我玩过一点点，但实在是太辛苦了...). 而既然 type class 可以，用 ML 的 module 应该也是可以的。 是否还有其他的方式，以及他们的 expressiveness 方面我就不是很 清楚了。你知道其他的吗？ :) --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 140.109.20.217