2019年/12月/28日
类型的复杂
Programming languages are a fascinating area because they combine computer science (and logic) with many other disciplines including sociology human computer interaction and things that cannot be scientifically quantified like intuition, taste and (for better or worse) politics.
编程语言是一个引人入胜的领域，因为它们将计算机科学（逻辑）与许多其他学科结合在一起，包括社会学，人机交互以及无法科学量化的事物，例如直觉，品位和（无论好坏）政治。
When we talk about programming languages, we often treat it mainly as scientific discussion seeking some objective truth. This is not surprising - science is surrounded by an aura of perfection and so it is easy to think that focusing on the core scientific essence (and leaving out everything) else is the right way of looking at programming languages.
当我们谈论编程语言时，我们通常主要将其视为寻求某种客观真理的科学讨论。 这不足为奇-科学被完美的光环围绕着，因此很容易想到，专注于核心科学本质（并忽略所有其他事物）是看待编程语言的正确方法。
Bertrand Russell introduced types in a paper Mathematical logic as based on the theory of type in 1908 to avoid logical paradoxes arising from self-reference.
Bertrand Russell 在1908年基于类型理论在论文《数学逻辑》中引入了类型，以避免自引用引起的逻辑悖论
In ML-like languages, types denoted sets of values that a computation can produce
在类似ML的语言中，类型表示计算可以产生的一组值。
TypeScript and Dart, which introduces safety holes like covariant generics
TypeScript and Dart两种语言，会引入协变安全漏洞
In summary, a type is not a formal concept that can have a precise definition.
总之，类型不是可以具有精确定义的形式概念
interesting work does not necessarilly need complex theory: “there have been important observations in the history of science, which have included no theoretical assumptions at all.”
有趣的工作不一定需要复杂的理论：“科学史上有重要的发现，根本没有任何理论上的假设。”