codedump的电报频道

#书

每年的4.23是世界读书日，推荐一本过去一年在精读的技术书《Types and Programming Languages》（简称TAPL）。

我与这本书的缘分是这样的：

最开始，想要看懂databend里面的表达式系统代码，看迟先生的类型体操系列文章《用 Rust 做类型体操》，发现看不懂。

于是请教了负责表达式系统的同事，给我推荐了TAPL这本书。

开始阅读TAPL，但是发现里面很多符号看不懂，需要补一些数理逻辑和Lambda演算的基础。

补习了上述基础之后，继续看TAPL，能看懂部分了。第一刷TAPL花了半年多的时间（包括补习基础的时间）。

现在又重新整理了一下之前做的笔记，也看了部分EOPL（全称“Essentials of Programming Languages”）的内容，开始第二刷。在完善了前面的基础之后，第二刷就流畅很多了。

这个过程中有如下的收获：
1、体验到了数理逻辑形式化的美感。做工程的时候，经常会做工程上的trade-off，但是在类型系统这里，一个类型能否转换为另一个类型，需要严谨的推导，可以就是可以，不行就是不行，不存在trade-off。我特别喜欢这种符号形式化、确定性的美感。
2、重拾了对PL的兴趣。我接下来会把EOPL和TAPL刷完，打算接着学习一下OCaml，再看看能不能给Rust贡献一些代码。
3、后面会学习抽象代数和范畴论，学习范畴论是为了更好理解PL里面的一些理论。
4、Rust最开始吸引我的是它的内存安全特性，现在除此以外，还有它强大的类型系统，强类型系统的语言写起来放心、方便很多。我后续可能不太能接受用非强类型的语言来做为主力编程语言了。

为了纪念这个学习的过程，我前两个月趁着JD搞活动，花重金（大几百人民币）买了一本TAPL原版书，五一之后就能送到了。

www.tg-me.com/sg/telegram/com.codedump_notes/555

3.7K views老C, Apr 23, 2024 at 03:52

#书

每年的4.23是世界读书日，推荐一本过去一年在精读的技术书《Types and Programming Languages》（简称TAPL）。

我与这本书的缘分是这样的：

最开始，想要看懂databend里面的表达式系统代码，看迟先生的类型体操系列文章《用 Rust 做类型体操》，发现看不懂。

于是请教了负责表达式系统的同事，给我推荐了TAPL这本书。

开始阅读TAPL，但是发现里面很多符号看不懂，需要补一些数理逻辑和Lambda演算的基础。

补习了上述基础之后，继续看TAPL，能看懂部分了。第一刷TAPL花了半年多的时间（包括补习基础的时间）。

现在又重新整理了一下之前做的笔记，也看了部分EOPL（全称“Essentials of Programming Languages”）的内容，开始第二刷。在完善了前面的基础之后，第二刷就流畅很多了。

这个过程中有如下的收获：
1、体验到了数理逻辑形式化的美感。做工程的时候，经常会做工程上的trade-off，但是在类型系统这里，一个类型能否转换为另一个类型，需要严谨的推导，可以就是可以，不行就是不行，不存在trade-off。我特别喜欢这种符号形式化、确定性的美感。
2、重拾了对PL的兴趣。我接下来会把EOPL和TAPL刷完，打算接着学习一下OCaml，再看看能不能给Rust贡献一些代码。
3、后面会学习抽象代数和范畴论，学习范畴论是为了更好理解PL里面的一些理论。
4、Rust最开始吸引我的是它的内存安全特性，现在除此以外，还有它强大的类型系统，强类型系统的语言写起来放心、方便很多。我后续可能不太能接受用非强类型的语言来做为主力编程语言了。

为了纪念这个学习的过程，我前两个月趁着JD搞活动，花重金（大几百人民币）买了一本TAPL原版书，五一之后就能送到了。

BY codedump的电报频道