Re: [問題] GADT 概念
抱歉，最近一直沒能來，回復得晚了。
※ 引述《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
討論串 (同標題文章)
PLT 近期熱門文章
PTT數位生活區 即時熱門文章
