Re: [心得] Dependent Type "簡"介

看板PLT (程式語言與理論)作者godfat (godfat 真常)時間17年前 (2007/10/01 17:07)推噓1(1推 0噓 0→)

留言1則, 1人參與討論串3/5 (看更多)

剛趕完一個工，來賺點 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: ggreif@gmail.com -- 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