豆瓣读书：https://book.douban.com/subject/30247790/
本书是2018年出版的《The Little xxx》系列的一本新书，
其他耳熟能详的“小人书”有很多，
例如，The Little Schemer，The Seasoned Schemer，
The Little MLer，The Little LISPer，The Little Prover，等等。
这本书在圈子里一直饱受关注，人们经常谈论官网和Github仓库的动态，
这是由于网络上介绍Dependent Type的资料还比较少。
但其实Dependent Type也并不陌生，使用Idris，可以简单的体验一下。
言归正传，如果有一些Scheme和Haskell的基础，
读这本书可能会更容易一些。
该书虽然称为The Little，但是却厚达400多页，
已经算是一本中等厚度的书了，所以读起来需要一定的耐心。
书中照例采用了一问一答的方式来编写，
首先介绍了什么是type，type constructor，data constructor，
以及normal form（实际上是weak head normal form）。
然后第一个比较重要的概念出现在P53，就是U（the universe type），
因此我们就可以在P98，使用Π来绑定类型变量了，
相当于类型理论中的universal types。
由于是Dependent Type，
所以Π绑定的参量既可以是一个具体的类型，也可以是一个值。
接下来的章节比较乏味，主要是在归纳集上进行归纳证明。
用到了自然数集和List，对皮亚诺算术或者递归论熟悉的朋友这里可以不看了。
可以直接到P129看Vector，这是一个最常见的Dependent Type的例子。
然后在P143引出了本书的主题，Dependent Type的定义。
Dependent Types A type that is determined by something that is not a type is called a dependent type.
笔锋一转，从P174开始，书的内容焕然一身，
引出了Curry–Howard correspondence，虽然书中没显式的说明，
但“程序就是证明”的思想，跃然纸上。
这样一来，书的内容也就丰满多了，
在P220介绍了 Σ （即类型理论中的 existential types）之后，
就可以完成很多命题的证明了，作者给出了大量的示例（还是归纳集上的）。
最后介绍了Either，Maybe，（the sum type），
然后在P295介绍了Trivial（the unit type），
以及P302，Absurd（the empty type / bottom type）。
该齐的都齐了，作者在书的末尾，
写了如何证明“不存在xxx使得zzz成立的”的方法（其实就是使用Absurd）。
然后内容就结束了。
对Pi语言感兴趣的，可以直接翻到P357，有一点点介绍，
对Dependent Type的实现方式感兴趣的，可以翻到P363。
本书作为一本类型理论的“小人书”，
茶余饭后，值得轻松一读。
若有收获，就点个赞吧
0 人点赞
