本文是讀完oopsla16的一些心得
上面這個測試例運行的結(jié)果是茧痒，main函數(shù)中拋出一個ClassCastException，異常信息為 “java.lang.Integer cannot be cast to java.lang.String”。原因簡單說就是因為JVM運行時檢查出了類型問題谎柄，發(fā)現(xiàn)代碼企圖將一個Integer類型的對象轉(zhuǎn)化為String類型觉鼻，這種轉(zhuǎn)換是不允許的。
但是棋凳，這種類型問題本應(yīng)該是在編譯期檢查出來的拦坠。這里是什么導(dǎo)致編譯器檢查不出這個類型錯誤？
我們模擬一下Java類型推導(dǎo)的過程剩岳。類型推導(dǎo)總是先假設(shè)程序類型是對的贞滨，然后在這個前提下得出一些條件，最后驗證這些條件是否成立拍棕。用類型Z代替Constrain<U, ? super T>中的晓铆？，可以得到Figure 2中的信息绰播。
a)和b)是顯而易見的骄噪。c)是因為upcast函數(shù)的第一個參數(shù)的類型是Constrain<A, B>， 而這里傳入了一個合法的參數(shù)蠢箩，參數(shù)類型為Constrain<U, ? super T>链蕊。由于將U作為Bind的類型構(gòu)造符事甜，所以得到Z==B。upcast第二個參數(shù)的類型為T滔韵，而聲明的類型為B逻谦，因此得到T<:B，因為B<:A奏属，這里A已經(jīng)因為Bind<U>而變?yōu)閁跨跨，因此B<:U。
對于c), d), e)3個條件囱皿，F(xiàn)igure-1的例子中c)是滿足的勇婴，因為upcast接受了一個合法的Constrain<U, Z>類型的參數(shù)。由于c)條件滿足嘱腥，所以d)和e)也滿足了耕渴。
但是， Figure-1的正確僅僅是一個巧合齿兔。原因是Java類型推導(dǎo)驗證條件的順序是不確定的橱脸。如果順序的驗證條件c), d), e)，那么條件滿足分苇。如果先驗證d),e)添诉，再驗證c)，那么T<:U這個條件就不能滿足了医寿。所以不同編譯器在編譯Figure-1時結(jié)果是不同的栏赴。
不過我個人認為，造成這種類型推導(dǎo)結(jié)果不一致的原因并不能完全歸結(jié)于條件的驗證順序靖秩。如果Java像Ocaml一樣嚴格的區(qū)分Some和None须眷，那么對于Figure-1的例子，我們就不可能向upcast函數(shù)傳一個合法的Constrain<U, ? super T>類型的對象沟突。
oopsla16中還給出了一些其他例子花颗，用于說明Java類型推導(dǎo)的不一致性。
Ocaml 實現(xiàn)
type ('a, 'b) eq = Refl : ('a, 'a) eq
let cast (type a) (type b) (eq: (a, b) eq) (x : a) : b =
match eq with
| Refl -> x
let lies : (int, string)eq = Obj.magic 0;;
cast lies 42
上面的Ocaml也實現(xiàn)了一個與Figure-1一樣的問題的例子惠拭。執(zhí)行后內(nèi)存錯直接導(dǎo)致ocaml解釋器崩潰扩劝。不過與Java不同的是，構(gòu)造(int ,string)eq類型需要使用Obj.magic作為hack手段求橄，而Java直接使用null就可以今野。
結(jié)論
- Java的類型推導(dǎo)是難以捉摸的，因此使用時應(yīng)該盡可能的給出類型參數(shù)信息罐农。
- 強類型語言的確更安全一些。
參考文獻：
[1] Java and Scala’s Type Systems are Unsound
[2] Java's unsoundness (from an ML-ish point of view)
