技术,生活,随看 \随转
【作者】尼古拉斯·卡尔
【格式】#epub #mobi #azw3 #pdf
【分类】#计算机 #信息技术 #互联网 #脑科学 #科普
【简介】本书作者让人心悦诚服地认识到，所有的信息技术都会带来一种智能伦理。印刷图书如何让我们进入聚精会神的状态，从而促进深度思维和创造性思维的发展。相比之下，互联网鼓励我们蜻蜓点水般地从多种信息来源中广泛采集碎片化的信息，其伦理规范就是工业主义，这是一套速度至上、效率至上的伦理，也是一套产量最大化、消费最大化的伦理——如此说来，互联网正在按照自己的面目改造我们。本书中，有智能技术的发展历史，有大众科学的普及知识，有文化批判的真知灼见，全书处处闪耀着令人难忘的智慧之光，这些内容恰似对我们现代人的心智状态所做的全面而深远的拷问。这本书必将永远改变我们对传媒和大脑的思考方式。
📚 阅读：点击下载
📢 频道：@sharebooks4you
👥 群组：@sharing_books4u
#书单
微博上一位老兄列举了一堆学习类型系统的书，我转抄来电报，给每本书加上了豆瓣页面跳转，原微博地址：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的课程，据说结果惨烈，哈哈哈，但是我相信老师们会进化的；最终这些努力都会转换成产业里更好的软件质量和更高的开发效率。
微博上一位老兄列举了一堆学习类型系统的书，我转抄来电报，给每本书加上了豆瓣页面跳转，原微博地址：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的课程，据说结果惨烈，哈哈哈，但是我相信老师们会进化的；最终这些努力都会转换成产业里更好的软件质量和更高的开发效率。
The Rust Book 精简版
"这本书完全由人类编写——没有任何内容是由 ChatGPT 生成的" 😅
https://jasonwalton.ca/rust-book-abridged/#whats-different-about-this-book
"这本书完全由人类编写——没有任何内容是由 ChatGPT 生成的" 😅
https://jasonwalton.ca/rust-book-abridged/#whats-different-about-this-book
jasonwalton.ca
The Rust Book (Abridged) | The rs Book
账户抽象（AA）是一种设计方法，它大大简化和概括了web3钱包账户和交易在区块链系统中的处理方式。
今年东京EthGlobal黑客马拉松的获胜者之一，Ibrahim Ipek（Winngie Technologies的创始人）向Telo News解释说：
"账户抽象是一项改变游戏规则的技术，它允许开发者创建去中心化的应用程序，而不要求用户事先有加密货币的知识。它将在后台运行，让每个人都能无缝地使用钱包技术，就像使用Facebook或Twitter等社交媒体网站一样方便。该开发项目将取代目前复杂的钱包交易流程，允许无缝跨链互换，实现简化的工资支付，自动向传统银行账户脱钩，并将小额支付纳入社交媒体连接，所有这些都具有相同的简单web2用户界面。"
通常情况下，大多数区块链的默认账户是一个外部拥有的账户，由Metamask、公共和私人密钥对的组合来保证。虽然这种控制个人资产的方法对一些人来说可能令人生畏，但它是目前的规范。
被称为ERC-4337的新标准为开发者提供了创造新的、更灵活和用户友好的智能合约钱包的机会。打个比方，智能合约钱包类似于Gmail账户，它允许用户访问多个社交媒体账户。带有链外基础设施的验证逻辑，以及社交网络整合能力和委托加油的能力，使得智能合约钱包比外部拥有的账户有了很大的改进。
Polygon是计划在其产品和服务的生态系统中利用AA的主要加密货币协议之一。ERC-4337将把AA带到所有与EVM兼容的链上，如Arbitrum、Avalanche和Optimism。
@Telonews_cn | #Telo_原创
https://scenex.jina.ai/ 为每一张图片生成细致的文本描述
scenex.jina.ai
SceneXplain - Leading AI Solution for Image Captions and Video Summaries
Experience cutting-edge computer vision with our premier image captioning and video summarization algorithms. Tailored for content creators, media professionals, SEO experts, and e-commerce enterprises. Featuring multilingual support and seamless API integration.…
🏞 Image To Prompt：上传图片，自动生成 Prompt
🔗：Web
频道：@NewlearnerChannel
