F-subとJavaのGenerics
今回はちょっと難しい話を…。たぶんこれだけ読んでも意味不明です。
この前まで輪講で Types and Programming Languages を読んでいて、やっと輪講が終わりました。終わったと言っても、26章 Bounded Quantification までしか読んでいませんが。我々は型理論の専門家ではないので、この辺までで良いだろうという流れです。
26章は、Java の Generics でお馴染みのF-sub(F<:)が出てきます。汎用的な関数を作るときに、サブタイプだけだと、あるタイプのサブタイプを適用すると、型情報が落ちてしまいます。ポリモーフィズム(OOPで一般的なサブタイプポリモーフィズムではなくパラメトリックポリモーフィズム)を使うと、型変数にどんな型をも適用できるようになってしまうので、型エラーになってしまう場合がある。そこで、適用できる型の範囲を制限できるようにしようというのが、F-sub です。
Javaでいうと、Genericsを使えば、ArrayList
などからget
するときに、型キャストが要らなくなる…ということの理論的な話です。
この章では、Full F-subというのが出てきて、
if S1 <: T1 and S2 :> T2 then
∀X<:S1. S2 :> ∀X<:T1. T2
となります。さっきから出てきている<:
は、T<:S
でT
はS
のサブタイプであるという関係を表します。S1
とT1
の関係が直観に反しているのは、クロージャの引数の型(∀X
は型を引数に取るクロージャの型)と同じだと本文にも書かれています。
さて、ここからは自分の勘違いの話です。
このFull F-subを読んで、何を考えたのか Java の Generics のワイルドカード「?
」を思い浮かべてしまい、
JComponent :> JButton
なので、Full F-sub のルールに従うと、
ArrayList<? extends JComponent> <: ArrayList<? extends JButton>
であり、次のコードの (2) がOKで(1)がエラーになるはずなのでは?と考えてしまったのです。
(数時間悩みました)
ArrayList<? extends JComponent> list1 = ...;
ArrayList<? extends JButton> list2 = ...;
list1 = list2; //(1) OK
list2 = list1; //(2) エラー
勘違いの話はここで終わり。そもそも、Java でF-subの話を持ってくるなら、クラス定義の次のコードです。
class MyList<T extends JComponent> {
:
}
そもそも MyList<JButton> list3;
は何であったかというと、
これは ∀T<:JComponent. MyList
型を持つ値にJButton
という型を適用した型を持つlist
という変数の宣言でした。
では、ワイルドカード「?
」はというと、
MyList<? extends JComponent> list4;
はMyList
の型変数にJComponent
の任意のサブクラスの型を適用した型でした。(厳密な説明ではありませんが)
よって、MyList<? extends JButton>
は MyList<JButton>
や MyList<? extends JButton>
のスーパータイプになっているようです。なので(1)のような代入ができるわけです。(Javaでのサブクラスとサブタイプの違いの1つの例ですね)
ArrayList<? extends JButton>
をF-subの話に関連づけるのであれば、F-subでの戻り値の型のサブタイプ関係に基づいている…と考えなければいけなかったようです。
これが原因で、Genericsのことを色々調べたので、今度まとめてみようかな…。
Types and Programming Languages
Benjamin C. Pierce
Mit Pr 2002-02-01
売り上げランキング : 7904
おすすめ平均
型理論の入門に手ごろな一冊
Amazonで詳しく見る
by G-Tools
Firefox 3.5で最後のタブを閉じてもウインドウを閉じないようにする
Firefox 3.5にアップデートしました。プラグインの互換性は3.0に更新するときほど困らず、bbs2chreaderを最新のnightlyに更新してNightly Tester Toolsで強制インストール、.NETのAssistantとRealPlayerとAdblockが無効になったくらいです。Google Toolbarは動いてます。
さて、あるTwitterのFollowerの発言で気付いたことが…。ジェスチャで最後のタブを閉じるとウインドウも閉じるようになってました。Firefox 2.x くらいではそんな仕様で、どうにかして対策した気がしますが、思い出せません。とりあえず設定一覧を眺めてみると、それらしき項目が。
ブラウザのURL欄にabout:configと入力してEnter。普通の人はここで警告が出ます。browser.tabs.closeWindowWithLastTabという項目を探して、その右側にある値をfalseに変更。あとはブラウザを再起動するだけ。
もしかして、どこかにUIがあるのかな…。