https://www.zhihu.com/question/19918532

型別系統的一些概念，眾說紛紜，使用上也比較亂。有些東西，甚至不好嚴格定義。以下算學術界的一種相對“嚴格”的說法。

1. 先定義一些基礎概念
Program Errors
trapped errors。導致程式終止執行，如除0，Java中陣列越界訪問
untrapped errors。 出錯後繼續執行，但可能出現任意行為。如C裡的緩衝區溢位、Jump到錯誤地址

{

untrapped errors，致命性的錯誤（Error）：程式進入了死迴圈、遞迴無法結束、記憶體溢位等。這類錯誤只能在程式設計階段解決，執行時程式本身無法解決。只能依靠其他程式干預，否則會一直處於非正常狀態。

trapped errors，非致命性的異常（Exception）：除數為0、運算元超出資料範圍、檔案並不存在、欲裝入的類檔案丟失、網路連線中斷……這類錯誤是可以檢測和處理的，所以產生了相應的異常處理機制。

}

Forbidden Behaviours

語言設計時，可以定義一組forbidden behaviors. 它必須包括所有untrapped errors, 但可能包含trapped errors.

Well behaved、ill behaved
well behaved: 如果程式執行不可能出現forbidden behaviors, 則為well behaved。
ill behaved: 否則為ill behaved...

2. 有了上面的概念，再討論強、弱型別，靜態、動態型別

強、弱型別
強型別strongly typed: 如果一種語言的所有程式都是well behaved——即不可能出現forbidden behaviors，則該語言為strongly typed。
弱型別weakly typed: 否則為weakly typed。比如C語言的緩衝區溢位，屬於trapped errors，即屬於forbidden behaviors..故C是弱型別
前面的人也說了，弱型別語言，型別檢查更不嚴格，如偏向於容忍隱式型別轉換。譬如說C語言的int可以變成double。 這樣的結果是：容易產生forbidden behaviours，所以是弱型別的

動態、靜態型別
靜態型別 statically: 如果在編譯時拒絕ill behaved程式，則是statically typed;
動態型別dynamiclly: 如果在執行時拒絕ill behaviors, 則是dynamiclly typed。

3. 誤區

大家覺得C語言要寫int a, int b之類的，Python不用寫(可以直接寫a, b)，所以C是靜態，Python是動態。這麼理解是不夠準確的。譬如Ocaml是靜態型別的，但是也可以不用明確地寫出來。。
Ocaml是靜態隱式型別


靜態型別可以分為兩種：
如果型別是語言語法的一部分，在是explicitly typed顯式型別；
如果型別通過編譯時推導，是implicity typed隱式型別, 比如ML和Haskell


4.下面是些例子
無型別： 彙編
弱型別、靜態型別 ： C/C++
弱型別、動態型別檢查： Perl/PHP
強型別、靜態型別檢查 ：Java/C#
強型別、動態型別檢查 ：Python, Scheme
靜態顯式型別 ：Java/C
靜態隱式型別 ：Ocaml, Haskell