編程語言的類型系統爲什麼如此重要？

程序是類型的證實。

計算機程序是創建在計算機硬件和一系列規則、協議、規範、算法基礎之上的；

 

程序是創建在邏輯和嚴格證實基礎之上的；

邏輯學的基本要素是：概念、判斷、推理；

類型系統至關於邏輯和科學中的概念，在此基礎上才能進行運算和推理；

編程語言不過是創建了類型系統和在類型系統基礎上的一些列運算法則而已。

類型＋運算法則＋運算推演＝程序；

 

做者：匿名用戶

連接：https://www.zhihu.com/question/23434097/answer/42374622

來源：知乎

著做權歸做者全部。商業轉載請聯繫做者得到受權，非商業轉載請註明出處。

 

先匿了，我不肯定我說的好很差。
發現和《Types and Programming》說的如出一轍，不匿了
安全，有了類型系統之後就能夠實現類型安全，這時候程序就變成了一個嚴格的數學證實過程，編譯器能夠機械地驗證程序某種程度的正確性，從而杜絕不少錯誤的發生。
正面例子：Haskell、Rust
反面例子：C，動態語言

抽象能力，在安全的前提下，一個強大的類型系統的標準是抽象能力，能將程序中的不少東西歸入安全的類型系統中進行抽象，這在安全性的前提下又不損耗靈活性，甚至性能也能很優化。動態語言的抽象能力能夠很強，但安全性和性能就不行了。
泛型、高階函數（閉包）、類型類、Monad、Lifetime（Rust） 屬於這一塊。

工程能力，一個強類型的編程語言比動態類型的語言更適合大規模軟件的構建，哪怕不存在性能問題，可是一樣取決於前兩點。
對於編譯器來講能清楚程序的意圖，對於人來講也是如此 。一個函數或者相似的東西，說白了就是一個映射關係，Python 中這些映射關係都是沒有很明顯的約束，要靠約定和默契才能維持，對大型軟件來講這是不行的。一個優秀的強類型的程序，不少函數都不須要文檔，光看函數申明就能夠了。而在安全的前提下的抽象，也是不容易引起災難的。

---

不過，同時類型檢查和標註增長了學習成本和編碼時間成本（類型推倒不是萬能的），編譯不過也會挫傷初學者信心，不像動態語言上馬就能幹，邊幹邊學。不過我的以爲值。

 

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