型と集合
風邪引いた。
http://d.hatena.ne.jp/nowokay/20090308 をみてて思ったのですが、id:SiroKuro さんが議論していたことは
前提
- クラスの定義がまずある
- 任意のクラスの定義Dに対し、型type(D)が定義される
- 任意のクラスの定義Dに対し、クラスclass(D)が定義される
命題
- type と class は同型か
- (むしろ、type, classをどう定義すれば腑に落ちるか)
ということであると思ってて、ZFCっぽくない集合がどうとかって言うのは本質から外れるんじゃないかなぁ。もちろん制約のひとつであるとは思いますが。
クラス、値、型
「クラスは型である」は間違いである - SiroKuro Pageを読んで少し考えてみた。
とりあえず、私のボキャブラリでは「値」がないと型を説明できなかった。
まずは、値と型の関係を定義する。
- すべての値は型をもつ
- 型はその値に対する操作に制約を課す
- 型はその値に対する操作を規定する
で、次のクラスの宣言が対応する型と、その制約を定義する。
- クラスの宣言はそれと同じ名前を持つ型を定義する
- クラスの宣言はそれが定義する型に許された操作を規定する
最後に、インスタンスがその型に属することを定義する。
- クラスインスタンス生成式の評価結果である値は、その対象となるクラスの宣言が定義する型をもつ
普通の文脈だと、「クラス」って言う用語は「クラスの宣言」の意味でつかってて、「型(クラス型)」って言う用語は「クラスの宣言を指定するnominalな何か」の意味で使ってるイメージが強い(「たまにJavaScriptには型がない」という記述も見かける)。
なお、私は「クラス」「カインド」「ドメイン」をそれぞれ「型」に近い意味で使ってることがあります(それぞれちょっとずつニュアンス違いますけど)。なんかそんな感じでごっちゃになってるだけじゃないのかな、と思ったり。
クラスの宣言とクラス型がごっちゃになってるなら、どの辺に共通点があるのか知りたい。
javacでヒープ汚染せずに代入文だけでクラッシュ - その後
http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=6806876
javacでヒープ汚染せずに代入文だけでクラッシュ - しげるメモのバグレポ送ったら登録されてた模様。
コンパイラのカテゴリとして送ったはずなのに、JavaのSpecificationのバグとして登録されてる…。Evaluationの項にも書いてありますが、javac(というかJLS3)では、intersection typeがnon-reifiableでないという認識になってるみたいですね*1。たぶん、この前のバグは氷山の一角だと思います。
ちなみに、英語がひどいのは仕様です。
*1:クラスファイルの仕様を考えるとどう考えてもreifiableではないのですが
javacでヒープ汚染せずに代入文だけでクラッシュ
寝ようと思ったら思いついた。
public class Main { public static void main(String...args) { Comparable<?>[] c = method(1, 1L); } static <T> T[] method(T...ts) { return ts; } }
これ、javacで警告でないけど実行するとClassCastException発生。言語仕様違反です。
おそらく、new T[ ]するときにreifiableな型の配列作ろうとしてイレイジャ変換かけている(erase(lub(Integer, Long)) = erase(Number & Comparable＜...＞) = Number としている)のに、戻り値にそれ伝播させてなくてT[ ]のまま使ってる。
明日まとめなおす予定。
