2004-11-03 [長年日記]
λ. ghc の新しい機能 Generalized Algebraic Data Types (GADT)
かなり今更だが、Inemuri nezumi diary (2004-10-08) よりメモ。言うまでもないけど、これがあると Phantom Types とか普通に使えるようになるし、色々と嬉しそうだ。
詳しくは、"Wobbly types: type inference for generalised algebraic data types" を見ればよさそうか。
あと、モデルとしては dependent types の場合と同じようなものを考えればよいのかな……
λ. James Cheney 氏
Phantom Types の James Cheney 氏って AlphaProlog の人でもあったのか。ちょっとビックリ。
λ. アメリカ大統領選
個人的にはどっちかと言えば民主党よりも共和党に勝ってほしいと思ってるけど、さてどうなるやら。それにしてもアメリカの選挙は面白いなぁ。
日記とは関係ないんですが、RHG いくー？ 前借りた奴そのまんまだから。
行きまーす。多分。
参照されている The Fun of Programming の章を読んだ目から見ると、なるほど結局こういう形の syntax sugar にしたんだという気持ちだったり。<br>http://page.freett.com/shelarcy/diary_2004-10.html#the_fun_of_programming
りょーかい。
syntax suger としてではなく、ダイレクトに実装したものだと思ってました。syntax suger ということは、結局内部では「型の等しさの証明」を明示的に引数として受け渡してるって事ですか?
desugarされたのを見た限り(-ddump-ds)、type equalityの追加はしていないと思われます。<br>GADTの推論・チェックを通りさえすれば、あとは普通のデータ型と同等に扱えるのでは？
(日記のリンク先の本のページなどの)ソースを見れば分かる通り Haskell98 + 拡張環境下での Phantom Types を使った関数の定義の仕方は明白なのだから、内部的な実装はともかくとして実質 syntax sugar なんだろうという意味で感慨を呟いたつもりだったんですが、その辺曖昧でしたね。
tradさん。ありがとうございます。<br>やっぱりそうですよね。<br><br>shelarcy さん。<br>GADTが「Haskell98 + 拡張環境下での Phantom Types」の syntax suger というよりは、むしろGADT(= 本来の Phantom Types ?)のある種のエンコーディングが「Haskell98 + 拡張環境下での Phantom Types」だったと考える方が良いように思います。<br>ちなみに、"Phantom Types", http://citeseer.ist.psu.edu/cheney03phantom.html には以下のように書かれてますね。<br><br> Recently, Cheney and Hinze [6] and Baars and Swierstra [4] found that many of these features can already be implemented via an encoding into Haskell based on equality types comprising “proof” of type equality.<br> However, this encoding has several drawbacks:<br><br>- It imposes a high annotation burden on programmers, limiting its usability;<br>- it incurs unnecessary run-time overhead in the form of calls to the identity function;<br>- it requires a different equality type definition for each kind; and<br>- it is limited by the constraint-solving abilities of the underlying type-checker.
ふむ、そうですか。分かりました。
あっ、ポインタありがとうございます。
そういえば、The Fun of Programming のページの Chapter 12 のTerm.hsはapplyIdの定義が抜けてますね。applyId = from であることは、まあ自明だと思うけど。