#杂
关于数学学习，有两个观察：

* 即便一个人的数学知识储备到了高中数学层次，部分小学数学的奥赛题也不一定能解得出来；
* “鸡兔同笼” 是非常经典的小学数学奥赛题型，可是如果学到了初中数学，有了未知数、方程式的概念，这个问题就是非常简单的解二元一次方程。

这两个观察的思考是，过度在技巧中沉浸，很多时候意义不大，因为”技巧“的钻研是个无底洞；与此相对的是，很多问题当你掌握了更高级的工具之后（比如上面的二元一次方程之于鸡兔同笼问题）就能马上迎刃而解。

所以对大部分人来说，掌握了一门知识的基础概念、做了一定量的练习之后，就可以接着去追求往更高层次的知识，而不是过度沉浸在”技巧“中。如何判断对一个知识的掌握已经“足够”了，首先根据二八原则来，掌握最常用的八，其它的边做边学；其次，如果有这个领域的经典教程，那么编撰这套教材的人肯定在这个领域已经浸淫多年，书里的重点、练习做得差不多就好了。

把这个观察得到的方法论推而广之：很多时候我们关注于“解题”本身，慢慢得过于关注技巧、为鸡毛蒜皮的问题解决而沾沾自喜，以至于忘了往更高的层次去走。比如以前还在写C的时候，经常为解决某个内存引发的问题而沾沾自喜，这些问题放到Rust语言的设计里编译器就不会让这种情况出现，很多问题在用了另外的角度、有了别的视野、换了其它工具之后就不复存在了。

人生苦短，别把太多问题放在“解题技巧”上，很可能当视野打开之后，问题就不再是问题了。解题之前，不妨多问自己几个问题：这个问题非要解决吗，能不能换别的路线绕开它，有没有更好的工具辅助解决这个问题，下一次能不能避免出现类似的问题，等等。扁鹊三兄弟的故事里，扁鹊就是兄弟里最能解题的人，而他两个哥哥都能问题发生之前避免问题，所以他们能力更强。

最后，反过来看前几年出台政策把奥赛的热度打下来，我认为是有可取之处的。如前面的讨论，奥赛过度关注技巧，这可能也是中国为什么赢得这么多奥赛金牌却出不来几个知名数学家的原因之一：解题解到最后，并不能让你成为一个大家。

#播客
最近新出的一档程序员主播的播客节目 《硬地骇客》 ，《从个人兴趣到财务自由：独立开发者也可以这样做开源》 这一期专门聊了几个商业化做的不错的开源项目，我这才知道 Dracula 做为一个编辑器主题还能这么赚钱。

最后谈到的由HomeBrew作者发起的 https://tea.xyz/ ，这个专门针对开源项目的web3项目也很有意思。

#杂
我现在算是对Sqlite运行机制有一些了解了，想围绕着它的生态在此之上做一些个人项目，但是这个数据库产品是在C端被用得更多，而我的工作方向在后端，所以有没有平时用Sqlite的人能说说它用起来有哪些不太爽可以改进的地方，或者是它的相关工具（比如数据恢复、中文搜索功能），谢谢。

#杂
二八定律最伟大的地方，是告诉我们很多时候，世界运行的规律是“非线性”的：

* 可能努力了几年，前面几年基本没啥回报，到了第五年开始爆发性的收割；
* 工资的增长和工作年限没啥关系，也就是说不一定每年涨个10%，可能是前几年不怎么涨，积累够了一个跳槽就翻倍了。

等等。

经常看到一个词“学生思维”，就我个人的体会，学生思维里常见的误区就是认为这个世界是“线性”的，比如认为努力就一定有回报，这可能跟学生在学校的“反馈”环境很有关系：去解决有标准答案、且指定范围的问题。离开了学校之后，面对的很多都是开放性的、没有标准答案的问题，于是二八定理告诉你，努力不一定马上有回报，或者说回报不一定马上能看得见。

成年人的世界里也不是完全没有线性反馈的事情了：锻炼就是一件能线性反馈的事情。能有线性反馈的事情，相对来说都是“容易”的：只管去做，做的过程中一直有反馈，得到的正反馈又能马上推进你继续做这件事情，而做非线性的事情就更加考验人，这可能也是很多成年人会喜欢朋友圈里发健身图的原因之一吧。

这周日（4.16）晚上八点，飞书群线上沙龙：Databend ｜ Rust编译优化小技巧，大家不见不散

#数学
圆周率π是最常见的两个无理数之一（另外一个是自然常数e），数学上已经对这些无理数的意义做了充分的解释。《疑犯追踪》S02E11中男主对π的解读是最浪漫的：

Student Girl: My Friend Has A Question, Mr. Swift . “What Is Any Of This Good For, And When Would We Ever Use It?”

(The Class Laughs.)

Finch : Let Me Show You. Π. The Ratio Of The Circumference Of A Circle To Its Diameter . And This Is Just The Beginning. It Keeps On Going. Forever. Without Ever Repeating. Which Means That Contained Within This String Of Decimals Is Every Single Other Number. Your Birth Date, Combination To Your Locker , Your Social Security Number. It’s All In There Somewhere. And If You Convert These Decimals Into Letters, You Would Have Every Word That Ever Existed In Every Possible Combination. The First Syllable You Spoke As A Baby, The Name Of Your Latest Crush , Your Entire Life Story From Beginning To End. Everything We Ever Say Or Do, All Of The World’s Infinite Possibilities Rest Within This One Simple Circle . Now What You Do With That Information, What It’s Good For, Well, That Would Be Up To You.

“Pi 一个圆的周长与它的直径的比，但不仅是这些而已，还有更多，永无止境，毫无重复。小数点后的这一串数字，每一个都是单一个体，你的生日、寄物柜锁密码、社会保险号码，都在这一串数字某处。如果你把这些数字转换成字母，你会得到每一个词，在每一个可能的组合中出现，你婴孩时开口讲的第一个音节、你心上人的名字、你从头至尾整个人生的故事、所有我们说的话和做的事…这个世界所有无尽的，可能性都在这个简单的圆里。你拿这些信息做什么…有什么用处…全都取决于你。”

B站上截取出来这一集的相关视频。

补充信息：但是π目前并没有证明是一个正规数（Normal Number），即数字显示出随机分布，且每个数字出现机会均等的实数，也就是说：虽然π是个无理数，但是也不能保证任意数字一定会出现在这个无理数的数字序列里。

#Databend
Databend最近搞了一个side project：AskBend。

这个项目依赖于Databend Cloud来存储Databend官网的文档数据，喂给OpenAI之后，生成一个可以根据文档内容回答问题的“客服机器人”。这个项目本身也开源了：https://github.com/datafuselabs/askbend，我的另一位同事把项目用在了自己的博客上：https://ask.xuanwo.io/，可以看到效果也不差。

另外今天看到一篇文章，有同学参考这个项目给PG也加了类似功能：https://al-assad.github.io/posts/replicate-askbend-on-postgres/

我开始在想：给sqlite做一个类似功能，好像也不赖吧，毕竟我最近也在找可以做的sqlite周边生态产品。


Reference：
* https://t.me/codedump_notes/429

#Databend
从2021年初成立公司到今天，经过两年多的打磨，Databend Cloud终于要在2023年4月20日这天 官宣发布 了。

#剧
去年无意间看到的一部剧 《破事精英》 ，情景喜剧类节目，剧情设定是一个公司里最不起眼、各种破事的“破事部”发生的故事，讨论了很多职场话题：PUA、中年危机、职场性骚扰等，当时看的时候抱着60分就好纯打发时间的念头去看，实际追完觉得能有个75分。里面甚至有个工作机器人起名叫“盯盯乐”，要是这部剧是阿里旗下优酷出的话，那效果能拉满了，属于去年看过的剧里最为惊喜的一部，眼看着 第二季 就要出来了。

#杂
《A Tutorial Introduction to the Lambda Calculus》，关于lambda演算的一个简明教程，只有17页。

#类型系统
#书单
微博上一位老兄列举了一堆学习类型系统的书，我转抄来电报，给每本书加上了豆瓣页面跳转，原微博地址：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