不懂 Type Theory 或 Category Theory 仍称自己学 CS 是否为「民科」？

看讨论的问题是什么。如果没学过Type Theory就对编程语言设计指手划脚，那么确实与民科没啥区别。长久以来编程语言的问题都好似“怎么说都有理”，但类型论告诉我们关于编程语言确实有一些solid，backed by science的claim可以作。这种情况下对于这些claim和它们的理论选择视而不见，确实是很民科了。

我说的就是某些Golang的狂热教徒。8102年了还用product type表示本该是sum type的东西（err!=nil）还觉得这是语言优势恕我直言不能接受。

== Edit == 2.20

我觉得有必要心平气和地聊聊PL的人是怎么看待语言设计的问题，这在知乎这个聊到某某语言设计的问题里，一半都懂CuTT一半只有工程背景的大环境下还是很应该的。

评论区有人提到说golang的err的设计并不是“错误”，而是纯粹的taste问题。我恕不能赞同。但同时也不得不承认即使在9201年要argue类型对于一门语言是essential而且critical的，同时不诉诸于taste，是件非常困难的任务。

我想那位知友表达了一个很常见的对于type theory之于编程语言的作用的批评：我们可以argue说type safety提供了safety，但有人同样可以argue选择safety而不是别的问题本身就是taste。Harper认为type不safe的语言都不make sense，而CSAPP的一个作者Bryant说Standard ML这样的东西纯粹就是没法用来写“Fast code”。可能做PL的人自然而然得觉得如果程序的行为是unspecified或者non-deterministic的本身就已经是ridiculous/unacceptable了，同时我们很在意语言的表达力，抽象能力等。但system的人可能就觉得只要是方便build system的东西就很好，其他的性质都不是很care。后面这样的朋友很可能是不懂（也不关心）类型论的，但如果拒绝他们参与语言设计的讨论（并且称之为民科）似乎也是过于傲慢了。

对于这个，我的观点是这样的：9201了设计一门语言往往有一个核心目标，这个目标可以是PL框架下的（比如我要语言可以被形式验证，或者我希望语言是lazy的），也很可能不是PL框架下的（比如Go的设计目标中一大部分是“好用”且及其高效的并发）。对于后者，很可能最终的语言是要牺牲safety的（想想rust的unsafe）。但我们同时也得承认，在满足了核心目标之后，语言有也有很大一部分的设计是浮动的。对于这样的部分，type theory可以指导如何增强抽象能力，如何使程序员少犯错误等等。Go就是典型的在后者上fuxx up了。我不会批评为什么Go还有null pointer exception这种陈年烂账（以及语言是unsafe的），因为很大程度上这是Go向它的核心目标妥协的结果。但err!=nil的设计纯粹就是不应该了。结论就是，如果你一点type theory都不懂就做语言设计，你也许会获得一个满足你的核心需求的语言，但你的语言的很可能非常难用而且四处是坑。这样的产物被叫做民科很可能是不冤的。