1樓：Jason Hu
incompleteness theorem已經決定了程式語言理論裡很多東西都是不可兼得的。難道這個領域還缺乏想把所有事情都做盡結果所有事情都做得一無是處的例子嗎？乙個好的語言應該只有乙個核心理念，做多了的都是假的。
2樓：
連DT都沒有你說個鬼。。。
Polymorphism不就乙個型別引數，還有Haskell那堆forall，rank-N也是。
Typeclass這種低階的東西用instance argument就能搞定。
ML那個module也就寫個record的事。
還有何必過分追求type inference，多寫個引數和返回型別又不會死→_→
3樓：
我建議你改一下問題名字或描述，你這描述十句不離type inference，敢情type inference在乙個型別系統中的地位有這麼重要？推導的時候把全稱量詞丟最外面不就得了，想要Rank-N自己寫個函式簽名也不是什麼難事吧，Type inference的解決方案已經很成熟了，Haskell那種級別的就夠用，除了在let或lambda這些地方特別需要Type inference，其他地方直接寫簽名多好啊，清晰、易讀。Type System還有這麼多值得探索的東西，槓在Type inference這種地方簡直就是浪費時間。
PS: 這裡的Type Inference特指在語言內，需要編譯器去做的符號推導的。在靜態分析領域Type Inference還是非常重要的。
程式語言中內建型別是怎麼實現的？
Yunfei Lu 都有。一種語言，首先有基本型別，其實就是資料在記憶體的布局，方便表示不同種類的資料，例如整型和浮點是一定要有的，因為cpu的規範。再組合得到陣列，函式型別等，再發展出代數型別，然後包裝成介面 類 泛型等高階概念。基本型別在編譯器裡規定。至於標準庫中定義的型別，通常是某種組合的封裝...
為什麼說 C 語言是系統級程式設計的首選？
打醬油的瘋子 基本上都沒有說到點子上。C語言基本上就是彙編的直譯，不能更簡單了。整個C就是指標和位址，然後是數值運算，別無其他。唯一隱藏的就是暫存器分配。再多一點就是提供了彙編沒有的型別驗證保護，而這個也是可以去掉的，C語言真的不能再多了。再多說一句話，就是基本上彙編能做的C能做9.5成，最後0.5...
如何證明乙個語言的型別系統是sound的？
Jason Hu 我一直很想系統地寫一篇這個回答。我趁現在沒啥事我就開個頭吧。操作語義 指稱語義 代數語義 公理語義學，誰能簡單介紹下？這裡我都用STLC舉例。denotational semantics denotational semantics的原理是找到乙個數學模型，然後證明你的type s...