抱歉，最近一直没能来，回复得晚了。 ※ 引述《noctem (noctem)》之铭言： : 哇，高手来了。都是很有意思而且不很容易答的问题哩。 :) 哪里是高手，PLT里水太深了，随便一个topic後面都有一堆我不懂的东西 : 先确认一下我们说的 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 是对的。 一般实践里常用的应该就是这种简单形式的吧，因为这个技巧比较直观， 在现有的type system里又是完全valid，有助于安全性，所以很多项目 的代码里都可以见到。 : 这样的 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 这个First-class phantom type看起来挺有趣，有空打算读读第一篇paper， 谢谢。 : : 3) 如果不考虑value-dependent types，而只限於type-dependent : : types这一范围， 除了GADT还有哪些其他的type arithmetic是可以 : : 加到今天的程序语言里的呢？ 在这一范围内，表述能力最强的类型系统 : : 是怎样的呢？ : Hmmm... 我只知道在以前用 Haskell 的 type class 也可以做一些 : type arithmetic (我玩过一点点，但实在是太辛苦了...). : 而既然 type class 可以，用 ML 的 module 应该也是可以的。 : 是否还有其他的方式，以及他们的 expressiveness 方面我就不是很 : 清楚了。你知道其他的吗？ :) 我也不清楚，只知道一个MLF http://gallium.inria.fr/~remy/mlf/ 这里是example http://pauillac.inria.fr/~lebotlan/mlf/mlf_eng.html#prototype 和tutorial http://gallium.inria.fr/~remy/mlf/mlf-for-everyone.pdf --

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