作者godfat (godfat 真常)
看板PLT
標題Re: [心得] Dependent Type "簡"介
時間Mon Oct 1 17:07:22 2007
剛趕完一個工,來賺點 p 幣...
如果後來有把東西都整理好的話,會釋出這次的一些 action script 3 code,
名稱定為 avatar block, 顧名思義就是放一群 avatar 的 block,
原始模型是 flickr 的照片 flash, 不過我加了很多擴充的東西。
action script 3 比 2 好用滿多的,但還是有非常大的不足就是了...
※ 引述《jaiyalas (ZZZ)》之銘言:
: 據說,這個版的版主之前有嘗試過以這樣的方式來實做
: 也許可以請版主大人稍微講一下實做的心得 = =+
如果我沒記錯的話在 C_and_CPP 講過滿多的 ccc
不過後來懶了,就很少在那邊發言了。
其實我是覺得概念很簡單啦,基本上就理解成 meta-programming 就好了。
不過要用 C++ template 做 meta-programming, 其實限制很多,
做起來時常會讓人有腦爆感。而且 dependent on value, 幾乎可以說只對數字有效。
像是假設這樣:
clas NaturalNumber{};
template <NaturalNumber n>
class List{};
這樣是不行的!
因為 NaturalNumber, 包含所有的 class, 都只能在 runtime 去 construct,
而 template 是完全 compile-time 的東西,兩者不能混著用。
再來看 factorial 吧 XD
template <int N> class fact{
public:
enum{ value = N * fact<N-1>::value };
};
template <> class fact<1>{
public:
enum{ value = 1};
};
這裡定義了兩種 fact, 上面的 fact 是 generic 的,
也就是一般的 template. 而下面的,叫做 template specialization,
有點像是 case of 的味道吧,當 N = 1 時,不使用泛用的 template,
要求使用特製的 template. 而 C++ 在還沒真正用到 fact 時,
不會做完整的 semantic 檢查,只有部份的 type check,(當然 syntax check 會做)
直到真正要用時,才會做第二階段的檢查,這叫 two-phase lookup,
這細節很多很複雜,而且也不是這裡的重點,所以就不多說了... @_@
不過微軟的 VC 就是沒做 two-phase lookup 的最好例子 XD
(2008 會不會做不知道,依照慣例大概是沒有吧 XD)
C++ 強調 early error, 所以要求 two-phase lookup, 但是非常難實做,
所以微軟第一階段的檢查忽略不做。
anyway, 當我們呼叫:
fact<10>::value
時,compiler 就會去檢查 10 符不符合哪個 template specialization?
答案是沒有,所以 fact<10> 會去 instantiation 最泛用的那個 N,
然後去計算他的 value 等於多少?
這邊 compiler 又會發現,value 是 N * fact<9>::value,
於是他再去計算 fact<9>::value 是多少?
...
最後 compiler 會找到 fact<1> 是某個 specialization,
他的 value 會是 1, 然後就能夠把 fact<10>::value 計算出來。
於是你的程式裡面就會有 10 個 class, 分別是:
fact<10>, fact<9>, fact<8>, ... fact<1>
這 10 個 class 在 runtime 上分別是不同的 class,
所以用 template 時常會有 code bloat 的問題...
但在這個例子中,最佳化良好的話,其實一個 class 都不會產生。
因為 compiler 會發現 fact<10>::value 是個常數,
而其他地方都沒有用到 fact<...>...,
所以 linking 時就會全部捨棄了。
唉呀呀,有事,待續...
: Omega http://web.cecs.pdx.edu/~sheard/Omega/index.html
: 沒有試過,只有看過程式碼
: 感覺語法和Haskell很像
我是覺得算是擴充 haskell 吧?
godfat ~ 3.2$ port info omega
Omega 1.4.2, lang/Omega (Variants: universal)
http://web.cecs.pdx.edu/~sheard/Omega/
Omega is a strict dialect of Haskell providing type-level computations
and by this virtue integrates a theorem prover.
Build Dependencies: ghc
Library Dependencies: readline
Platforms: darwin freebsd
Maintainers:
[email protected]
--
Nobody can take anything away from him.
Nor can anyone give anything to him.
What came from the sea,
has returned to the sea.
Chrono Cross
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 61.218.90.242
1F:推 jaiyalas:推簽名檔,好久沒碰了..Orz 10/01 17:15