Telegram Group & Telegram Channel
#书

每年的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原版书,五一之后就能送到了。



tg-me.com/codedump_notes/555
Create:
Last Update:

#书

每年的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的电报频道




Share with your friend now:
tg-me.com/codedump_notes/555

View MORE
Open in Telegram


telegram Telegram | DID YOU KNOW?

Date: |

What is Telegram Possible Future Strategies?

Cryptoassets enthusiasts use this application for their trade activities, and they may make donations for this cause.If somehow Telegram do run out of money to sustain themselves they will probably introduce some features that will not hinder the rudimentary principle of Telegram but provide users with enhanced and enriched experience. This could be similar to features where characters can be customized in a game which directly do not affect the in-game strategies but add to the experience.

The STAR Market, as is implied by the name, is heavily geared toward smaller innovative tech companies, in particular those engaged in strategically important fields, such as biopharmaceuticals, 5G technology, semiconductors, and new energy. The STAR Market currently has 340 listed securities. The STAR Market is seen as important for China’s high-tech and emerging industries, providing a space for smaller companies to raise capital in China. This is especially significant for technology companies that may be viewed with suspicion on overseas stock exchanges.

telegram from us


Telegram codedump的电报频道
FROM USA