类型 vs. 类型检查
引言
这篇文章是一些经常复用的常识科普的总结。
经问题太多，不得不绕过其它地方直接在这里填坑。
虽然对于内行可能很多废话，但是仍然建议自上而下阅读（发现有梗请按字面意思理解）。
阅读之前的另一个建议：姑且不要盲信某些问答或百科网站的观点，待足够了解相关话题后自行评估自洽性。
本体论(Ontology)
先问是什么，再问为什么。
不自觉地忽视“类型是什么”这个问题是造成乱象的根源之一，所以有必要首先澄清——尽管内容或许会（很遗憾地）出乎很多读者的意料。
概述
高屋建瓴：类型是一种抽象的实体(entity) 。嗯，等于没说。
当然其实是说了些什么的。熟悉 C++ 基本概念（字面意思，语源是 ISO/IEC 14882 Clause 6以前是3 的标题）知道，至少类型不是名称，是被指称而不是指称别的什么玩意儿的——在几乎所有语言和习惯用法中都一致。
不过现实中的问题破事当然不那么简单。
类型 = 分类？
当然不是。
在说为什么不是之前，首先需要正视这是一个有些年头了的笑话，并且可能具有名人效应而带坏一些不明真相的小碰友，典型地如这篇。在一口一个类型系统(type system) 如何如何时，不觉犯了基本的没搞清概念的内涵的低级错误，以至于把名义类型系统(nominal type system) 和类型系统混为一谈。鉴于LtU 上的评论已经足够一针见血，不在此多科普细节。
讽刺的是，造成这种误会的原因，恐怕就是原文批判的：类型系统烂设计过于有存在感——而影响了作者本应具有的视野。这样，应予以重视的教训除了“不要在不懂的领域跑火车”外，更要紧的是得先搞清楚要批判的东西到底是什么玩意儿，而不是一上来就想造个大煋闻，批判一番了事——不仅削弱本来可能性以微粒子程度存在的观点的合理性还误导群众，而且容易贻笑大方。
那么一个类型“到底是什么玩意儿”？
还是先不用急。这一节的重点是理解“到底什么玩意儿”这个说法。
其实这是一个哲♂学问题，确切地说是一个形而上学问题（不管对这个领域清楚不清楚，请忘记黑格尔的私货，总之这里的意思和辩证法没一腿）。
这类统称本体论问题的重点就是“是什么”。接下来，有意思的是，要指望谁来回答这个问题？对于一般形式来讲，的确可能只能哲学到底了，但对于某个类型系统中的类型——这种人为设计中的一份子，其实答案是很明显的：类型系统的设计者或者类型的设计者（类型系统的用户）说“我就是想要让它叫那个啥”，如是而已。
比较无奈的是，很多钦定类型“是什么”者自己就对这层含义并不怎么清楚，似乎自以为是天赋人权了。
这个之后再提。先看一下祖宗长什么样再说吧。
历史上的“类型”是什么玩意儿
这段历史常识可能很多童鞋不知道，虽然真要追根溯源可能倒未必出很多人意料。
讨论当代程序设计语言使用的“类型”的直系高祖——其实本质上就是个哲学（数学）范畴的问题，因为“类型”是为了解决第三次数学危机（罗素悖论）搞出来的副产品——类型论的研究对象。
按照罗素本人的一些努力构造的解法之一是创造一个公理系统——请注意其中的“类(class)”和“面向对象”等并没有毛线关系（要是习惯望文生义可能就像上面提的搞不清什么是类型的那位一样中招了）。虽然作为事后诸葛亮，主流数学到现在也并不吃这套（而改用 ZF(C) ），但还是不妨提一些存在间接的深刻影响，特别是“类”的概念——比如 NBG（嗯不是某一心一教……）以及“一般化的抽象废话”涉及的一些重要基础（虽然这块东西即便是 Haskell 厨也并不方便抡圆了用）。
意义何在？
那么这些历史与上面有什么关系呢？嘛，至少对名义上的本体论意义，其实就是——毫无关系。
且不提当年的副产品发展到现在还在兴风作浪要顶掉集合论篡数学基础的大位，就是仅在程序语言理论中，它仍然是王道正统的几乎不二的形式基础。但是，纵观古今，我愣是没发现有一个类型论在一般意义上来指导用户应该或必须把（具有类型论以外性质的）什么东西抽象成什么类型。也就是说，本体论意义的“类型”，根本就没有指导类型系统设计一般的数理逻辑理论支持，更不用提强调本体论意义的必要性了。具体地，各种类型论中，并没有要求“类型”如同所谓面向对象的类一样，成为和某种领域外实体的对应，以作为建模或“分类”的基础，而仅仅是（重写意义上的）项(term) 上关联的一些抽象实体罢了。（像 C++ 的 tag dispatching 之类的所谓奇技淫巧，反倒更符合“类型”在这里的原意—— term 上的 tag ——虽然语言规则使之具有的性质并不怎么方便用。）
某些人使用语言时没人限制该干啥，仗着指哪打哪、叫啥是啥可以作为天赋人权来用（看起来像是鸭子类型么……），强制让一个类型和一个不符合（类型系统蕴含的）一般性质的本体对应还想甩锅给类型系统的设计？这甩锅路线也太烂了……
从这里更加可以看出之前的例子为什么是笑话。强要加给“类型”以含义的，明明是没怎么搞清需求以及很可能对类型系统如何在编码时起作用一窍不通的用户，而并不来源于类型系统自身的设计。反过来，符合这些上梁不正的需求的类型系统“设计”，倒极可能带来更高渣设计的语用风险——比如说，解决一类明明在设计目标领域内的（其它语言容易做到的）问题怎么用都麻烦，让用户怀疑人生之类……
派生概念
出了偏差是要负责任的……
还需要补课。
类型正确(Type Correctness)
因为上梁不正的观念偏差，钦点“正确”的风气大势所趋严重；可惜排除少数几个坑明显特别大、涉及用户基数也大的话题（如 const correctness ），一个个都不怎么喜欢定义清楚什么叫“正确”……
当然，把“正确”当成“符合期望（上层规格说明隐含的规则）”其实在实用时本身问题不是很大。
比较显著的问题直接来源于上述的本体论认知混乱导致的对语用习惯的干扰：要先知道“是”什么类型，才敢放心用。然而，这并不总是有必要；无条件遵守这个教条反而容易引入不被期望的错误。
病例集中体现在类型推断（这里 inference 译为“推断”指要求必须存在能用于确定项上类型指派的解否则失败，通译“推论”没有这层含义，而“推导”(deduction) 形式上更一般但更弱，一般不要求限制特定输入的形式）上。典型例子是 C# 提供了 var 关键字，“社区”意见迅速分为两派（中间派似乎惯于闷声大发财）：尽量用和尽量不用。虽然前者主要势力之一的 Reflector 党忍受性能拙计（也许他们都有 SSD ）我不是很能理解，切入点也非常奇怪，但整体还是算有那么些道理；而后者主要理由是不显式写出类型可读性差之类。
基于足够的理由，我旗帜鲜明地站在前者一边——谁告诉你看不出显式的类型可读性就差了？谁规定显式类型就是所谓“可读性”了？又有谁规定理解程序源代码片段的含义应该先从了解具体的项的某一个类型开始？说白了，不讲清楚前提非要这样胡扯的，或者没有理性思辨就以不准确的直觉断定这种依赖是无条件必要的，都显然不适应缺乏阅读缺乏显式类型标注(type annotation) 代码；考虑到程序设计语言发展的历史以及所谓动态语言的流行，这样的人的阅读代码的天赋或经验本身就显得相当可疑，由此而来的片面结论也就缺乏普遍的参考价值了。基本原理其实很简单：根据没有刻意混淆过的代码理解程序是正向的工程过程，理应和产生设计思路在方向上大体一致。考察程序或语言自身的设计如何满足需求这一过程，都是先有表达设计的程序或语言（不管是合乎文法的代码还是先于代码成型的模糊概念），后有约束和刻画程序中局部组成部分的类型（附加的元信息）及依附于类型语义的类型系统规则。（这个过程就是一般意义上所谓的 typing ，不过这部分内容不在这里剧透，以下另行详细讨论。）并且，普遍意义上，后者是可选的，缺少类型的描述不应使被描述的设计不完整，否则设计本身就有问题（例如，对用于描述设计的语言选型不当）。当然，某些情况下（如设计具体类型系统的规则时），“类型”本身是“业务”对象，但这类情况下“类型”就是“值”，而真正起作用的类型是描述系统的元语言中的元类型——如果需要这种类型存在的话。总之，不管这里的过程由人类读者还是由机器根据语言的具体规则进行实现，缺乏这种先来后到的逻辑常识（换种说法，“允许使用类型简化问题”的需求和“引入类型”的设计之间满足因果律），对任何理解类型怎么在高级语言中工作来解决实际问题的用户来说，都是说不过去的。
另一个支持使用类型推断代替显式类型的观点声称这便于代码重构。实际上，这是上述逻辑自然的推论：若想在代码中表达的逻辑本来不就依赖具体的类型，那么以某个阶段为基础，无视这种类型继续重复微调正向设计自然不应受到更多的限制。不过，这已经是一种弱化的描述。更合适的做法是，即便不管实际会发生多少重构需求，多数情况下就不应该写出（即便是不重复的）显式类型，因为这些情况问题的有效的解就不依赖类型具体是什么；显式依赖不必要的具体类型不必要地限制了解的外延，反而在类型正确的问题上更不精确（或者说，错误的程度更大），只是在重构时更容易发现不够精确才更容易暴露出来而已。而作为上述因果律的应用，本来正常解决问题的套路就是先理顺逻辑和实体之间的关系然后考虑能在选定的语言中使用什么类型，而不是先看看自己知道些某种语言能支持什么本体论意义上的名义类型然后去凑解决方案（如果只是因为选定的语言抽象起来实在太不方便，那是选型失败，是工程缺陷，没权没条件改掉就横竖都得忍）。后者虽然在推敲具体实现时作为妥协（如消歧义文法变通和照顾编译性能）无可厚非，但显然是方法论意义上的颠倒因果，而且很容易造成抽象泄漏)这类擦屁股后患无穷的问题。而这里依赖类型推断就是表达必要关系（而不是本体）的有效手段（如果只是编译器报错烂就别赖方法论问题了）。
小结：上面这种情况把类型写得太清楚具体，反而是不那么“类型正确”的——不“合适”地符合解决问题的“期望”。
简而言之，更清楚地限制使用的类型具体“是什么”，依赖不必要的从实现泄漏的假设，导致很可能更不正确。这是一个长期以来容易被用户普遍忽视的过度设计/实现的典型例子。
类型识别(Type Identification)
提到“是什么”的问题，最显然的实现是比较给定的表示类型的数据结构（类型标识）和已知类型的对应数据结构是否相等。进一步地，也可以扩展到任意两个类型之间的同一性(identity) 比较。这也被一些语言直接提供为语言特性。
这种实现具体的操作也暴露了基于本体论意义上的判断的局限，而且被更多用于普遍地了解。比如说， C++ 中一般尽量不要用 typeid 比较相等——倒未必是因为运行时 typeid 性能低（至少存在比 dynamic_cast 普遍快的实现），而主要是因为硬编码 == 扩展性烂得太感人了，和 dynamic_cast 啊虚函数啊比起来没啥优势。
当然不可否认运行时类型识别不少情况下可能仍然有必要（对 typeid 而言，实现 any 这样的类型擦除(type erasure) ，算是个主要的例子），但是提可扩展性和灵活性其实是不太必要关心运行时不运行时，道理都是类似的。为什么这里的理解就出了偏差呢？谁的责任？
类型转换(Type Conversion)
可能是基于某些劣质教材和人云亦云等原因，有几个相关话题的认识是重灾区，值得单独拎出来挂的程度。
鉴于不是重点，仅举一例。
例如，许多童鞋甚至不知道强制(coercion) 是一种隐式转换以及多态(ad-hoc polymorphsim) 而和铸型(casting) 这种显式转换混为一谈。
至少，请停止颠倒黑白。
类型安全(Type Safety)
比起上面几个而言，类型“安全”是在一般语言中更普遍存在的口水话题。
所谓安全，基本含义和“正确”类似，仍然是“符合期望”，只不过更多地强调考虑风险而不是考虑具体对策评判尺度的唯一性，在一般意义上也相对不那么容易被语言规则强制。
按理说，既然选择措施的余地更大，就应该更容易有共识各取所需才对。可惜业界的坏毛病是信息不对等面不改色继续窝里斗——我所谓的安全和你所谓的安全，也许就是鸡同鸭讲，但这个没关系，不听我话的就是不安全的！（黑人问号……）
基本上，比较有实用价值的类型安全的定义，依赖于类型这个概念本身的含义的准确性上。此外，在使用场景下需要满足一些性质。（虽然并非内涵）从实用角度出发，保证一般程序的“安全”这种普遍的期望，不能总是指望人；也就是说这类安全的机制应设计为可以被人以外的工具自动地检查。和表达能力结合，这需要设计本身具有某种意义上的可编程性。
较常用的一种安全机制的基本思路是，定义类型是某个域(domain) 中值的集合，保证类型安全即约束需要考察的值总是符合某一些类型的约束。语言规则中的一部分通过公开和类型关联的构造（如表达式），使判断对象语言描述的程序是否符合类型安全这项任务能被程序表达和实现（包括语言自身的实现，如编译时的检查）。这样，类型安全可以视为某一些语言规则中蕴含的性质。当语言的规则不足以保证它表达的任意操作产生的值属于规则事先指定的值的集合之内，这些规则就不是安全的；反之，这些语言规则是类型安全的。
问题在于，这里有个关键的岔子：什么才算是符合预期的事先指定的规则？或者说，如何选取域？
虽然有一些较为公认的规则（而被不同语言“借鉴”），但因为依赖的假设和类型系统设计不尽相同，超过类似上面的周知陈述地去讨论什么才能算类型安全而取得共识这点在一定意义上是徒劳的。
作为典型症状，相当多数用户在得到他们认为“安全”性质的推理过程有相当大的漏洞：他们往往既不知道作为共识的安全性质是指什么，也不清楚（各种不同的）“安全”是如何保证的。这样的方法论对澄清这种本已经混沌的话题自然没什么卵用。
点题
回到标题的问题。
类型检查(Typechecking)
现实的类型安全一般通过在语言设计中由两类手段提供支持：语言的构造性规则限制不安全类型构造的表达，以及语言对潜在不安全的表达进行额外的语义检查。前者涉及对不特定的项（如表达式）进行类型指派，也就是一般所谓的 typing ；后者相对比较事后诸葛亮但在设计语言时配置起来比较灵活（可以很容易地弱到没有而不那么容易影响其它语义），所谓 typechecking ；然而很多人根本没搞清楚这两者根本不是一回事。
（终于点题了……）
应当注意，这两者根本上指的是涉及语言规则的设计而非直接指定语言实现的行为。特别地，尽管一般实现 typechecking 蕴含解一个判定性问题——即作用于代码上判断出一个表示“通过”或“不通过”的二元结果，却并不一定表示接受或者拒绝接受程序。一条语言规则不会因为实现要求附加其它行为或不要求任何可预测的行为（所谓未定义行为）而不适合归类为 typechecking 规则。举例： C 的许多使用非兼容类型(compatible type) 的值的操作是未定义行为，这不是 typing ，而指定了作用于指针类型上的 typechecking ；只是它的要求弱到允许检查是空实现——实现可以附加任意少的检查操作（直至进行可能无法预料的响应）致使其可用性未必符合一般对 typechecking 有效性的期望，而容易被误认为和 typechecking 无关。
一般来说，这两者的确具有不少共性才容易被混淆。比如说，都可以作为实现某种类型安全规范的要素；再如，简单情形下都可以构造为判定性问题；再如，在语言实现的哪个阶段(phase) ——翻译时（“静态”）还是运行时（“动态”）检查（注意区分出“运行时”和非“运行时”并非对所有语言都有意义）；不一而足。只是混淆这两者问题可能还不大，但基于混乱的认知对语言设计分类而只能让围观群众继续不明觉厉，就不那么好笑了。
静态/动态（类型）？
首当其中的是一些关于静态/动态语言和静态类型/动态类型语言的混乱。在了解 typing 之后这就不攻自破了：静态类型或者动态类型都和 typing 的时机有关；而单纯静态/动态，对彻底不提供类型系统设计的 typeless 的语言都可能说得通。
重复，需注意，对一些不规定区分静态/动态阶段的语言，这些分类都毫无意义——除非就干脆认为静态只是特殊的动态得了。
强类型？
更严重的问题在于“强类型”(strong type/strong typing/strongly typed) 这个说法。考虑到这个概念词源上基于 typing ，引用起来却杂糅了 typing 和 typechecking ，不同作者对什么是足够强的理解还不一样，混乱可见一斑。
这里的一般建议是避免混乱的用法。如果不能避免，仅在确定类型时使用，而讨论类型检查时直接以具体的机制（对 ××× 类型的检查）来避免混乱。特别地，应注意避免“弱类型”这样望文生义还模糊了原本可能已分清界限而使之失去实用价值的生造词。（后者的使用者通常还具有其它的认知混乱，比如无法区分强制(coercion) 和铸型(casting) ，不清楚强制可以作为一种多态(ad-hoc polymorphism) 而不一定有损类型安全性等等。）对特定实体声明保持类型的性质，使用 manifest typing/latent typing 论述——这样“强类型”这个说法才有一些无歧义的生存空间，不至于像“弱类型”一样鸡肋且造成误会。
另外，虽然不如上面的提法直接，还有其它一些观点指出强类型和类型检查的“强度”无关。和上面的结论类似，为了避免不相关的误导，持有这类观点的作者也同样不建议使用“强类型”“弱类型”的说法。
习题
了解这里的习惯描述以后，仍然可能未必了解概念的使用（因为没法指望不同的作者统一使用准确的含义），不过我期望读者能自行分辨一些较明显的混淆。
看似专业的错误面面观（当然，也不是每个作者都用错了）：
提示 首先，考虑讨论的是一般的语言设计，不要先入为主地假想类型（系统）已经存在。其次，“使用语言规则约束程序行为提供保证”的设计手段和“使用类型系统的某些性质提供保证实现这种设计手段”不是同一个层次的抽象。
延伸阅读
继续补课仍然是有意义的，特别是验证以上认知的意义。
另外，虽然不是惯常风格，偶尔留些习题也好。
类型可靠性(Soundness)
可靠性是关于逻辑系统的性质。一个逻辑系统是可靠的，当且仅当任意合式公式(well-formed formula) 论证的形式保证在语义上有效（有效前提蕴含有效结论）。
类型系统（或者，至少它的一个实现——确信符合要求的程序代码）可以作为逻辑系统，相应地具有类型可靠性。具有类型可靠性的类型系统，静态地（在运行前）通过类型检查得到程序的性质，和程序运行时保证的性质总是一致。
有些关于类型安全的命题可能足够众所周知之而被作为可靠性的公认判断准则，比如这个（嘛，函数类型对参数类型协变的公理，原文挂了暂时也懒得找）。遗憾的是可用的结论虽然普适但过于基础而太少，而且仍然依赖特定对象语言的类型系统设计（有些语言根本就不支持表达这样的类型所以就是一句空话……）。
强制类型(Mandatory Typing)
一般来说，一个语言设计可以有类型系统，不过还是有一些手段能在现有的语言上套用不同的类型系统并发挥原始设计者都并不一定预见的作用。
这样有个问题。如果把使用不同设计的类型系统作为扩展手段，那么原始的设计中坚持指定的类型系统有什么用呢？
当然，一致性(conformance) 是在写 spec 时的核心问题。不过，是什么决定，有必要把 spec 写成这样呢？意义何在，又有多少的部分是妥协？实践上通常采用哪些演进路线，决策的理由是？
语法方法主义(Syntacticism)
从逻辑系统的意义上来说，让类型检查的规则代替表达类型的类型指派规则是可行的。这种处理具有一定的普遍意义，同时（至少形式上）能减少通常无法准确形式化的语义规则带来的纰漏。极端地，可以用形式文法把语义规则用语法规则和前提假设代替。
然而，实际上局限也非常明显。
被忽视的重点在于，这以已经得到了一个可靠的形式系统——良型(well-typed) 规则为前提——这并非适用于一般领域（特别是通用目的语言的设计），类型系统的抽象能力并不足以应对所有需求变化。这对语言规范的维护者提出了不切实际的要求，以至于就给出规范的这个任务上都无法保证可实现。从工程角度看，不满足可行性要求是一种规约失败，即便限制通用性以保证能勉强设计出来结果，也只是个变通的妥协，根本算不上针对原需求的正确的解决方案。
其次，运行类型检查的算法复杂性和实现及维护良型程序需要的代价，往往没有被妥善考虑。这里的代价更多落在语言的直接用户上，使用户使用这样的语言的理由打了折扣，还（因为对语言的了解程度普遍不如设计者，以及基数较大）容易造成原本就没有解决的混乱急剧扩大——庸俗点说，可读性、可调试性、最小惊讶原则……这类也是一揽子口水话题了。
虽然当前没有完全分析归纳某些理论家在局限明显的情形下继续吹捧这类“完全体”静态类型语言的动机（也许是数理逻辑一向就有证明论语义(proof-theoretic semantics)方法学的间接影响……嗯……且不管和形式逻辑内的观点撕逼），不想阴谋论，不过作为问题也是有必要思考一下的：在一般意义下支持的理由（有什么优势以及能够接受的不足）？
结语
……科普教育果然还是甩链接省时省劲。