Abstract Types have Existential Type
id:sumii先生に，昨年の日記 id:flappphys:20041027:p1 にトラックバックをいただいた．丁寧にありがとうございます．
それこそ私が↑で始めて存在型に出合った Cardelli, On Understanding Types, Data Abstraction, and Polymorphism (PDF) でもよいのだけれど，原典ぽいものが見つかったので貼ってみる：
分かりやすそうなやつだと，講義録があった：
- http://www.cs.purdue.edu/homes/suresh/565-Spring2005/ CS565: Programming Languages
他にも google:"abstract type existential" で色々見つかる... と言っても「存在型が何であるか」が分かっている今だからこそこうして都合よい検索キーワードを選べるんだけどね．
ともかく，こないだ地下方面で正気の沙汰でない（ほめ言葉）スタックの実装が流行っていたようだが，ああいうのにおいて実装の詳細を隠してインタフェイスだけを公開するという仕組みにきれいに型付けするには存在型（∃α.τ）を使うのがよいってこと．AdaやMLがさきがけらしいけど，今で言ったらJavaのinterfaceやC++の抽象クラスか．
よくある例で... p: ∃α.(α×(α→int))とだけ書かれると，αが実際に何の型なのかは分からないので，例えばdouble型に対して使うsqrtとかstring型に対して使うprintとかはいかにも相性が悪い．だってαがdoubleとは縁もゆかりもない型かもしれないのに，そこに例えばsqrtを持って来ると，どうひねくって足掻いても「引数にする値はどこ？ どこなの？」となってしまう．こういう外界との付き合いの悪い型は，内輪同士で適当にやっててもらうしかない．つまり... pはタプルで，その前側要素の型がα，後側要素の型がα→intなので，後側を前側に適用することだけは（αが実際に何であっても）確実に可能だ： (snd p) (fst p) これを評価するとint型の値がきちんと返ることだけは確実．型∃α.(α×(α→int)) に対して考え得る操作というのはせいぜいこれくらいだ．
不便？ いや，これは「せいぜいこれだけの操作しかさせないように制限」するためには便利とも言える．「スタックを実装したパッケージ」が実はmainそのものを再帰呼び出ししてたり，キモいWindows APIだったりしたとき，中には触れて欲しくない．よって中身をあいまいに濁して誤魔化すために∃αを被せてしまうとよい．という訳でインタフェイスだけを公開した抽象型に使えます，ちゃんちゃん．
最初に私が構造体に使うのだと誤解したのは，抽象的なインタフェイスの定める「操作」は現実的には「中身」が伴ってないと役立たないので，必然的にそれらの組の型を持つことになり，例に出てくるのがタプル型ばかりだったため．しかしそれはあくまで結果であってそこがメインなんじゃないのよね．
...とまぁこの点についてはあの後ほどなく理解したのですが，「関数」の型にまつわる問題と（詳細までは結局分かりませんが），GJがJava 1.5そのものになったということは知りませんでした．
ああ，CS図書館にあったPierceが読みたい．と言うか，読む余裕が欲しい．と言うか，読む余裕を捻出できる程度に高い作業能力を持つ人間へと成長したい．
