你和我聊类型,谈语义,说你写OxCaml、写Scala、写Haskell,写Rocq、Agda、Lean,跟我说最近上ACM Digital Library又迪到了能媲美Lambda The Ultimate Imperative的论文,告诉我现在发现Philip Wadler也未必比得上北欧你连名都叫不上来的研究者,给我讲合一失败的痛苦、语义范畴的灵魂,抱怨现在只有依值类型和半结构化类型系统可以给你带来一丝丝的安全感,转头又说Dependent Pattern Matching写了至少三遍,最后还说最近写的有Effect System的东西才是真的好。怎么今天我打开你Github Stats一看:『Most Frequently Used Language:Go』