抱歉，最近一直沒能來，回復得晚了。 ※ 引述《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