#类型系统
#书单
微博上一位老兄列举了一堆学习类型系统的书，我转抄来电报，给每本书加上了豆瓣页面跳转，原微博地址：https://weibo.com/1683375645/Kk7Vr5yrr


整理一下关于类型系统的书籍。

Benjamin Pierce - Types and Programming Languages，是最好读的一本
Benjamin Pierce - Advanced Topics in Types and Programming Languages，这本写的比较散，不系统，但设计大量现代类型理论的课题

Hindley and Seldin - Lambda-Calculus and Combinators
Hindley - Basic Simple Type Theory

Hindley的第一本，应该是写给数学背景不错的计算机科学专业的学生的，非常系统的处理了几个有类型的λ系统；第二本则不是象它的题目所示，是关于Simple Typed Lambda的一般性理论，而是特别处理了一个Simple Typed Lambda系统，这个对深入学习Simple Typed Lambda系统的人来说是应该看的；

Barendregt - Introduction to Lambda Calculus
Barendregt - Lambda Calculus with Types

Barendregt差不多是Lambda领域最高学术权威。这两本书极其吃力，第一本和计算科学或者计算理论均无关，是纯数学，研究(untyped) lambda系统本身的特性（terms modulo convertibility），这本书的prerequisite比较恐怖，需要数理逻辑，集合论，拓扑，抽象代数，范畴；内容范围和Hindley的Lambda那本基本一致，但是烧死的脑细胞比Hindley那本多很多倍。

Barendregt的第二本是Typed Lambda，这个跟类型系统关系比较紧密一些；这本和第一本的关系不大，但有不少提到的地方。

Negerpelt and Geuvers - Type Theory and Formal Proof

这本也是数学专业的，但不是那么刚；而且它和证明论建立联系，应该是搞定理证明或者（类型系统）程序证明的人应该读的；比Hindley和Barendregt的书都好读而且内容更新；两个作者之一是Barendregt的学生。

Harper - Type Systems for Programming Languages
Harper - Practical Foundations for Programming Languages

Harper是卡梅的PLT权威，第一本不是书，介于一个Lecture Note和一个没写成书的草稿之间；第二本基本上是属于计算机科学领域的最刚的关于类型系统的介绍了，相当全面，但显然不会有数学书那么要求高了；这本应该算plt方面的最好教材。

++++

前面都是搞理论的，这里有几个可以实操的，是程序员们喜欢的方式。

Friedman and Christainsen - The Little Typer

这几天它我正在看这本书，是一本奇书；它实际上是在讲现代类型理论（Modern Type Theory，Martin Lof/Intuitionistic Type Theory，CICp in Coq, Luo's UTT, HoTT etc）中的一个特别的topic，叫Dependent Type的；简单的说Dependent Types允许你定义依赖于值的类型，但是定义的方式，在编程语言实现时，也是用操作值的代码实现的，而不是象例如C++的metaprogramming或者其他语言的generics一样使用另一套语法和操作符。

The Little Types构建了一个教学用的小语言，Pie；这个语言基于Racket平台，基本上你如果是搞语言研究，在开放平台上，Racket和Haskell是最多的选择，魔改ML也是个办法。学习Racket(Scheme)对于愿意花时间折腾语言的人来说应该是值得的，Racket有一套自己拓展语言的很好的框架和文档。

Stump - Verified Functional Programming in Agda

这是以Agda语言为例讲解在Agda里如何书写证明程序的，Agda也是General Purpose语言，但是很弱，就是不能实际开发应用。

Mimram - Program = Proof

这本也是讲了Agda的，但是只占其中一章；前半部分都是在讲基础知识，数理逻辑，Typed Lambda等，最后还有介绍HoTT的。

Brady - Type Driven Development with Idris

Edwin Brady是Idris语言的发明人，这个语言也是使用现代类型系统的（Luo's UTT），Idris是目前我知道的完全支持Dependent Type的语言里最Practical的一个，但仍然只是玩具级，开发不了复杂应用，但裸io和网络通讯还是有的，我看到Brady有论文写Web开发的。

++++

去Youtube上搜索Dependent Type，能找到Haskell社区开发者做的语言插件，还有Christainsen讲他的Pie；都有令人震撼的例子。

++++

我的桌面上还有一本四哥推荐的奇书：

Stepanov and Rose - From Mathematics to Generic Programming

书的作者是C++ STL类库的核心开发者；C++的Template实际上是一个图灵完备的系统，只是只能在Compile Time运行。它能做很多的事，但是做得非常困难。

C++没有前面说得这些现代类型系统，它是古早的nominal (or nominative) type system，当然很多新语言也仍然使用这个类型系统，包括Dart, Swift, Kotlin, Rust等等，但也有向未来迈进的，例如TypeScript就选择了Structural Type System（被Erik Meijer盛赞），还有Go这种奇葩的Duck Typing，你不知道未来会进化到哪里去，还有那么多的脚本语言，你也不知道是不是哪天哪些头脑发热的年轻程序员就给它们武装上一个现代类型系统。

换句话说，Stepanov的高超技巧，未来会在支持现代类型系统的编程语言里更容易实现，『飞向寻常百姓家』。

++++

在reddit/quora等社交网站上有很多关于现代类型系统的编程收益，以及它是一个大大的进步，还是和以前的类型系统进化一样，只解决了少少的问题但难度却陡增，有很多有益的讨论。

主流的观点和今天 @Puzzler_红叶 在另一个帖子里的回复一样，就是基于证明论和类型系统的语法方法，不如基于模型论的模型检查和模型验证方法；原因是后者的适用性更好。

++++

但我有不同的看法，我认为基于现代类型系统的编程语言将不可避免的进入产业，不但大流行，而且会产生深远的影响，只是这个时间不会太快，结果也未必太好，而已。原因如下：

1 类型系统是当前程序开发者的技能树中的东西，只要语言工具做得够好，应用并不是问题；而基于Model Checking技术写Spec完全跑到另一个Domain去了，除非老板安排，开发者没法支付去学习这个领域的知识的成本，也缺乏普适性。

2 在类型系统中进行数据合规/协议合规要求，是产业非常需要的东西，Idris语言作者给出的很多例子，开发者都看得懂而且很明确的知道，I need it；这样只要门槛不太高大家会去尝试和使用的。

3

象Haskell那样把很多数据结构塞进类型，还有要了老命的monad和do notation，不管开发者怎么吹捧，我都坚持认为是这些东西把Haskell语言给『毒』死了。

我用web技术打一个不算很恰当的比喻，web页面是三个东西构成的，html的layout，css的样式，操作dom的javascript实现交互和数据处理；如果设计者是个很嚼性的人，比如它坚持认为有脚本语言就够了，样式问题可以搞个像素系统，canvas，这web还能象今天这样流行吗？或者这个设计者是css大师，说不需要复杂脚本语言，交互都用css来搞定，它当然是『能』的，但问题是还有几个人愿意跟你一起『能』呢？

对吧。编程语言就象Web技术一样，要坚持多元化，Pluralism，要选择最恰当的技术解决它最擅长解决的问题。类型和证明当然不是包治百病，但是现代类型系统叠加函数式编程，它能向前进很大一步，让开发者觉得学习函数式编程和类型系统带来的工程收益是划算的，有一种还算符合直觉的方式可以编写程序的Constraint。

至于什么是并发的最佳原语，应该怎样在mutable/immutable之间找到平衡让数据结构即富有效率又不是过于抽象，那并不是类型系统要去回答的问题。那也许是通过其他技术来解决，使用其他理论。

基于以上的判断，我的理解是在可见的未来，不会很近但是也不会很遥远，现代类型理论的成果会深远影响编程语言；年轻的计算机专业毕业生会学会Agda/Coq这样的东西走出校门；知乎上貌似有人说waterloo给计算机专业本科生开了coq的课程，据说结果惨烈，哈哈哈，但是我相信老师们会进化的；最终这些努力都会转换成产业里更好的软件质量和更高的开发效率。

通过更好的类型系统解决更多的软件质量问题，是在过去三十多年的产业里梦寐以求的东西，因为缺乏良好的数学基础，只能催生出大量的工程技术解决问题；当然类型系统不是一帖灵，但是它肯定可以把软件质量，或者说程序员们能应对的系统复杂度，推到一个全新的高度。

#type theory# #type system# #dependent type#

#视频
科普视频，讲解了类型论的作用：《Why should you learn Type Theory?》

Reference：
* 类型系统推荐书籍

#项目
最近都在看类型系统的书籍TAPL，里面数学符号、公式很多，感觉Markdown在处理这种数学公式很多的笔记方面还是不够，于是开始用三脚猫的Latex来记一些笔记。

找到 李文威 老师开源的《代数学方法》项目中的一套Latex模板，感觉挺不错的，就照搬出来成了一个单独的项目，后续记Latex笔记都可以用得到：https://github.com/lichuang/latex-template 。另外《代数学方法》一书已经出版，所以老师开源的这套Latex代码，也可以作为学习Latex排版的一个不错的范例。

#生产力工具
之前好像并没有在电报频道里专门推荐过Relingo这款插件，今天专门写一下。

最开始了解到这个插件，是因为有网页生词提示、记忆的功能，感觉挺实用的，于是就第一时间买断了。

经过半年多的迭代，现在这个插件还能实时翻译youtube的字幕了，感觉这个功能也很实用。

除此以外在阅读英文网页的时候还可以翻译一段文字，外带提供的是DeepL翻译引擎的结果，光是DeepL的会员就值回票价了。

买得早所以当时100多就买断了，现在lifetime会员需要49刀的价格了。

#杂

出自微博：https://weibo.com/2167039312/N1lW7qoyE

#杂
北京时间2023年5月28日早上10:45分，国产大飞机C919商业首航。

Reference:
https://t.me/codedump_notes/420

#课程
继续我的类型系统（当前在阅读TAPL）自学之旅，找到几个以这本书为主要教材的课程及视频：

* 北大《编程语言的设计原理》：基本按照TAPL书上的内容来讲解的，可以认为划出了每章的重点。
* cornell的CS4110《Programming Languages and Logics》：有很多TAPL以外的内容，还讲了类型系统这部分内容的数理逻辑基础。
* cornell的CS6110《Advanced Programming Languages》：还没仔细看，不知道和CS4110有什么区别。
* 油管上的一个视频课程：内容挺好的，但是貌似没有继续更新了。

除此以外，暂时这类课程好像找不到其他视频类的教程了。

#人工智能
大概一个月以前看了一篇文字版本的陆奇对大模型的演讲，昨晚在B站闲逛找到了完整的视频，不过看起来视频和文章不是同一个演讲，但是总体来说看演讲视频效果还是能更好一些。

视频版：《陆奇最新演讲完整视频｜大模型带来的新范式》
文字版：《陆奇最新演讲实录：我的大模型世界观》

#项目推荐
crabviz：Rust写的基于LSP协议可以生成多种编程语言调用图关系的工具

https://user-images.githubusercontent.com/20551552/242812058-60584f59-a8f0-4a56-90eb-373c3f3b8cd5.gif

由于电报频道自带的搜索功能并不强大，所以我把数据同步导入了一份到：https://app.shokichan.com/c/tg/codedump_notes ，这里提供更强大的搜索功能。本频道的RSS订阅地址：https://rsshub.app/telegram/channel/codedump_notes

#高等教育
‘高等院校三千所’网页将以‘大规模集成网页(LSIP)’形式收录中国高校名单全集和网址，按照‘先中央后地方’、‘先本科后专科’的顺序形成中国高校层级图谱。针对普通高考录取，本页收录网址排除了成人高校，增补了港澳台高校，总院校链接数维持在三千左右。

#类型系统
《类型检查：时常被忽略的编译器组件》，个人觉得不错的一篇类型系统的科普文。

#文章
图灵奖得主 Richard W. Hamming《You and your research》的中文翻译稿

#数据库
慕尼黑工业大学数据库查询优化课程，搭配了600多页的 讲义。

#杂
高考可能是成年人面对的最后一个：有出题范围、有标准答案、限定时间内完成，又能给后续人生以极大影响的事情了。

从这个意义上来说，高考也难也不难，难的部分自不必说，不难是说高考的限制性很多、开放性很少。

等走向社会了，面对的很多都是开放的问题，而这些问题往往出题人是自己，做题人又是自己。比如XX的意义是什么，不同的人有不同的答案。其次没有了时间限制，答案会随着时间发生不同的变化。一个事情你20岁的时候也许做不到，努力到了30岁行不行？毕竟没有给你限制“答题”时间。这个问题反过来也是的，你20岁的时候能做到的事情，如果随着时间过去没有自己去对抗熵增，很可能过了几年能力就退化了。

很多人学生时代能考高分，出了社会不太行，我自己的观察就是不善于给自己出题，以前在学校都有明确的学习范围，出了社会得自己给自己找题目、找方向，他们也不善于回答没有标准答案的问题，习惯了被别人的标准答案（比如身边人、家里人、社会上）所裹挟。

总而言之吧，我读高中的时候老师经常给我们说：好好学习，等考上了大学随便你们玩，其实我即便到了高三还能经常下午放学了踢个一小时球，我怀念那种无忧无虑只为了一个有各种限定的答卷而努力的日子，这样的日子于我而言大概是不会再有了。

回到最开始的讨论，既然以后的日子可以自己出题自己解题，那么就连“高考能不能一考定终身”这个问题都值得去定义和解决了。

#Rust
早年学C++的时候，觉得如果只推荐一本C++的书，那一定是《Effective C++》，这本书总结了C++里最重要、常见的一些知识点，事实上我甚至认为任何领域都需要这样一本总结出最常见知识点的书。

如今网上有人写了一个《Effective Rust》出来，也是类似的思路。