类型系统中的反例

- 这篇文档面向类型系统（type system）有一定了解但想深入理解其局限性的读者。它列举了大量反例（counterexample），展示类型系统在某些场景下无法保证程序正确性。 - 类型系统是编程语言用来在编译阶段检查代码逻辑错误的一种机制——比如确保你不会把字符串当数字用。但它并非万能：即使通过类型检查，程序仍可能崩溃或行为异常。 - 作者通过具体代码示例（涉及 Java、TypeScript、Haskell、Rust 等语言），逐一展示类型系统中的「漏洞」——包括空引用（null reference）、类型强转（unsafe cast）、协变/逆变（covariance/contravariance）导致的运行时错误等。 - 这份读物对熟悉类型理论但缺乏实战边界情况的人来说很有价值，属于「类型系统防御性编程」领域的参考资料。