从工具的奴隶到工具的主人

摘要:我们每个人都是工具的奴隶。随着我们的学习,我们不断的加深自己对工具的认识,从而从它们里面解脱出来。现在我就来说一下我作为各种工具的奴隶,以及逐渐摆脱它们的思想控制的历史吧。

当我高中毕业进入大学计算机系的时候,辅导员对我们说:“你们不要只学书本知识,也要多见识一下业界的动态,比如去电脑城看看人家怎么装机。”当然他说我们要多动手,多长见识,这是对的。不过如果成天就研究怎么“装机”,研究哪种主板配哪种 CPU 之类的东西,你恐怕以后就只有去电脑城卖电脑了。

本科的时候,我经常发现一些同学不来上数学课。后来却发现他们在宿舍自己写程序,对MFC之类的东西津津乐道,引以为豪。当然会用MFC没有什么不好,可是如果你完全沉迷于这些东西,恐怕就完全局限于Windows的一些表面现象了。

所以我在大学的时候就开始折腾Linux,因为它貌似让我能够“深入”到计算机内部。那个时候,书店里只有一本 Linux 的书,封面非常简陋。这是一本非常古老的书,它教的是怎样得到Slackware Linux,然后把它从二三十张软盘装到电脑上。总之,我就是这样开始使用Linux的。后来我就走火入魔了,有时候上课居然在看GCC的内部结构文档。后来我又开始折腾TeX,把TeXbook都看了两遍,恁是用它写了我的本科毕业论文。

后来进了清华,因为不满意有人嘲笑我用Linux这种“像DOS的东西”,以及国内网站都对Windows和IE进行“优化”的情况,就写了个“完全用Linux工作”。确实,会Linux的人现在更容易找到工作,更容易被人当成高手。但是那些工具同样的奴役了我,经常以一些雕虫小技而自豪,让我看不到如何才能设计出新的,更好的东西。当它们的设计改变的时候,我就会像奴隶一样被牵着鼻子走。

这也许就是为什么我在清华的图书馆发现《SICP》的时候如此的欣喜。那本书是崭新的,后面的借书记录几乎是空白的。这些看似简单的东西教会我的,却比那些大部头和各种 HOWTO 教会我的更多,因为它们教会我的是WHY,而不只是HOW。当时我就发现,虽然自认为是一个“资深”的研究生,学过那么多种程序语言,各种系统工具甚至内核实现,可是相对于SICP的认识深度,我其实几乎完全不会写程序!在第三章,SICP 教会了我如何实现一个面向对象系统。这是我第一次感觉到自己真正的在开始认识和控制自己所用的工具。

因为通常人们认为Scheme不是一个“实用”的语言,没有很多“库”可以用,效率也不高,而Common Lisp是“工业标准”,再加上Paul Graham文章的怂恿,所以我就开始了解Common Lisp。在那段时间,我看了Paul Graham的《On Lisp》和Peter Norvig的 《Paradigms of Artificial Intelligence Programming》。怎么说呢?当时我以为自己学到很多,可是现在看来,它们教会我的并没有《SICP》的东西那么精髓和深刻。开头以为一山还有一山高,最后回头望去,其实复杂的东西并不比简单的好。现在当我再看Paul Graham和Peter Norvig的文章,就觉得相当幼稚了,而且有很大的宗教成分。

进入Cornell之后,因为Cornell的程序语言课是用SML的,我才真正的开始学习“静态类型”的函数式语言。之前在清华的时候,有个同学建议我试试ML和Haskell,可是因为我对Lisp 的执着,把他的话当成了耳边风。当然现在用上SML就免不了发现ML的类型系统的一些挠人的问题,所以我就开始了解Haskell,并且由于它看似优美的设计,我把“终极语言”的希望寄托于它。我开始着迷一些像monads,type class,lazy evaluation 一类的东西,看Simon Peyton Jones的一些关于函数式语言编译器的书。以至于走火入魔,对其它一切“常规”语言都持鄙视态度,看到什么都说“那只不过是个monad”。虽然有些语言被鄙视是合理的,有些却是被错怪了的。后来我也发现monad, type class, lazy evaluation这些东西其实并不是什么包治百病的灵丹妙药。

但是我很不喜欢Cornell的压抑气氛,所以最后决定离开。在不知何去何从的时候,我发了一封email给曾经给过我fellowship的IU教授Doug Hofstadter(《GEB》的作者)。我说我不知道该怎么办,后悔来了 Cornell,我现在对函数式语言感兴趣。他跟我说,IU的Dan Friedman就是做函数式语言的啊,你跟他联系一下,就说是我介绍你来的。我开头看过一点The Little Schemer,跟小人书似的,所以还以为Friedman是个年轻小伙。当我联系上Friedman的时候,他貌似早就认识我了一样。他说当年你的申请材料非常impressive,可惜你最后没有选择我们。你要知道,世界上最重要的不是名气,而是找到赏识你,能够跟你融洽共事的人。你的材料都还在,我会请委员会重新考虑你的申请。IU 的名气实在不大,而Friedman 实在是太谦虚了,所以连跟他打电话都没有明确表态想来IU,只是说“我考虑一下……”这就是我怎么进入IU的。

Friedman的教学真的有一手。虽然每个人对他看法不同,但是有几个最重要的地方他的指点是帮了我大忙的。有人可能想象不到,在Scheme这种动态类型语言的“老槽”,其实有人对“静态类型系统”的理解如此深刻。也就是在Friedman的指点下,我发现类型推导系统不过是一种“抽象解释”,而各种所谓的“typing rule”,不过是抽象解释器里面的分支语句。我后来就通过这个“直觉”,再加上Friedman的逻辑语言miniKanren里面对逻辑变量和unification的实现,做出了一个Hindley-Milner类型推导系统(HM 系统),也就是ML和 Haskell的类型系统。虽然我在Cornell的课程作业里实现过一个HM系统,但是直到Friedman的提点,我才明白了它“为什么”是那个样子,以至于达到更加优美的实现。后来经他一句话点拨,我又写出了一个lazy evaluation的解释器(也就是Haskell的语义),才发现原来SPJ的书里所谓的“graph reduction”,不过就是如此简单的思想。只不过在SPJ的书里,细节掩盖了本质。后来我在之前的HM系统之上做了一个非常小的改动,就实现了type class的功能,并且比Haskell的实现更加灵活。所以,就此我基本上掌握了ML和Haskell的理论精髓。

可是类型系统却貌似一个无止境的东西。在ML的系统之上,还有System F,Fw,MLF,Martin Lof Type Theory,CIC,……怎么没完没了?我一直觉得这些东西过度复杂,有那个必要吗?直到Amal Ahmed来到IU,我才相信了自己的感觉。然而,这却是以一种“反面”的方式达到的。

Amal是著名的Andrew Appel(“虎书”的作者)的学生,在类型系统和编译器的逻辑验证方面做过很多工作。可是她比较让人受不了,她总是显得好像自己是这里唯一懂得类型的人,而其他人都是类型白痴。她不时的提到跟Bob Harper, Benjamin Pierce等类型大牛一起合作的事情。如果你问她什么问题,她经常会回答你:“Bob Harper说……”她提到一个术语的时候总是把它说得无比神奇,把它的提出者的名字叫得异常响亮。有一次她上课给我们讲System F,我问她,为什么这个系统有两个“binder”,貌似太复杂了,为什么不能只用一个?她没有正面回答,而是嘲讽似的说:“不是你说可以就可以的。它就是这个样子的。”后来我却发现其实有另外一个系统,它只有一个binder,而且设计得更加简洁。后来我又在课程的 ailing list 了一个问题,质疑一个编译器验证方面的概念。本来是纯粹的学术讨论,却发现这封email根本没有发到全班同学信箱里,被Amal给moderate掉了!

看到这种种诡异的行为,我才意识到原来学术界存在各种“帮派”。即使一些人的理论完全被更简单的理论超越,他们也会为“自己人”的理论说话,让你搞不清到底什么好,什么不好。所以后来我对一些类型系统,以及Hoare Logic一类的“程序逻辑”产生了怀疑。我的课程project报告,就是指出Hoare Logic和Separation Logic所能完成的功能,其实用“符号执行”或者“model checking”就能完成。而这些程序逻辑所做的事情,不过是把程序翻译成了等价的逻辑表达式而已。到时候你要得知这些逻辑表达式的真伪,又必须经过一个类似程序分析的过程,所以这些逻辑只不过让你白走了一些弯路。当Amal听完我的报告,勉强的笑着说:“你告诉了我们这个结论,可是你能用它来做什么呢?”我才发现原来透彻的看法,并不一定能带来认同。人们都太喜欢“发明”东西,却不喜欢“归并”和“简化”东西。

可是这类型系统的迷雾却始终没有散去,像一座大山压在我头上。我不满意Haskell和ML的类型系统,又觉得System F等过于复杂。可是由于它们的“理论性”和它们创造者的“权威”,我不敢断定自己的看法就不是偏颇的。对付疑惑和恐惧的办法就是面对它们,看透它们,消灭它们。于是,我利用一个independent study的时间,独立实现了一个类型系统。我试图让它极度的简单,却又“包罗万象”。经过一番努力,这个类型系统“涵盖”了System F, MLF 以及另外一些类似系统的推导功能,却不直接“实现”他们。后来我就开始试图让它涵盖一种非常强大的类型系统,叫做intersection types。这种类型系统的研究已经进行了20多年,它不需要程序员写任何类型标记,却可以给任何“停机”的程序以类型。著名的Benjamin Pierce当年的博士论文,就是有关intersection types的。没几天,我就对自己的系统稍作改动,让它涵盖了一种最强大的intersection type系统(System I)的所有功能。然而我却很快发现这个系统是不能实用的,因为它在进行类型推导的时候相当于是在运行这个程序,这样类型推导的计算复杂度就会跟这个程序一样。这肯定是完全不能接受的。后来我才发现,原来已经有人指出了 System I 的这个问题。但是由于我事先实现了这个系统,所以我直接的看到了这个结论,而不需要通过繁琐的证明。

所以,我对类型推导的探索就这样到达了一个终点。我的类型系统是如此的简单,以至于我看到了类型推导的本质,而不需要记住复杂的符号和推理规则。我的系统在去掉了intersection type之后,仍然比System F和MLF都要强大。我也看到了Hindley-Milner系统里面的一个严重问题,它导致了这几十年来很多对于相关类型系统的研究,其实是在解决一个根本不存在的问题。而自动定理证明的研究者们,却直接的“绕过”了这个问题。这也就是我为什么开始对自动定理证明开始感兴趣。

后来对自动定理证明,Partial Evaluation 和 supercompilation的探索,让我看到那些看似高深的Martin Lof Type Theory, Linear Logic等概念,其实不过也就是用不同的说法来重复相同的话题。具体的内容我现在还不想谈,但是我清楚的看到在“形式化”的美丽外衣下,其实有很多等价的,重复的,无聊的东西。与其继续“钻研”它们,反复的叨咕差不多的内容,还不如用它们的“精髓”来做点有用的事情。

所以到现在,我已经基本上摆脱了几乎所有程序语言,编译器,类型系统,操作系统,逻辑推理系统给我设置的思维障碍。它们对我来说不再是什么神物,它们的设计者对我来说也不再是高不可攀的权威。我很开心,经过这段漫长的探索,让我自己的思想得到了解放,翻身成为了这些工具的主人。虽然我看到某些理论工具的研究恐怕早就已经到达路的尽头,然而它们里面隐含的美却是无价和永恒的。这种美让我对这个世界的许多其它方面有了焕然一新的看法。一个工具的价值不在于它自己,而在于你如何利用它创造出对人有益的东西,以及如何让更多的人掌握它。这就是我打算现在去做的。


本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.mzph.cn/news/450660.shtml

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

记录A component required a bean named ‘studentService‘ that could not be found.

前些天发现了一个巨牛的人工智能学习网站,通俗易懂,风趣幽默,忍不住分享一下给大家。点击跳转到教程。 报错如题: A component required a bean named studentService that could not be found. 出问题的代码行: &l…

Java---利用程序实现在控制台聊天

一.普通版(不能实现随意输入) 电脑A(服务器端) package day; import java.net.ServerSocket; import java.net.Socket; import java.text.SimpleDateFormat; import java.util.Date; import java.util.Scanner;public class Mysever {public static void…

16.看板方法——三类改进机会笔记

00.三种常见的模型和它们一些变种:约束理论及其主要理念;还有聚焦于分析和减少变异性的模型及其变种等。 01.五步聚焦法 *a.识别约束 *b.作出决定,以最大化利用约束 *c.使系统中的其余一切部分都服从于b中做出决定 *d.突破约束 *e.避免惰性&a…

C/C++的64位整型

在C/C中,64为整型一直是一种没有确定规范的数据类型。现今主流的编译器中,对64为整型的支持也是标准不一,形态各异。一般来说,64位整型的定义方式有long long和__int64两种(VC还支持_int64),而输出到标准输出方式有pri…

记录 Duplicate spring bean id dubbo

前些天发现了一个巨牛的人工智能学习网站,通俗易懂,风趣幽默,忍不住分享一下给大家。点击跳转到教程。 启动工程 报错如题: Duplicate spring bean id dubbo ,意思是id 重复。 原因是我在加载配置文件时加载了两个…

1.KafKa-介绍

转载于:https://www.cnblogs.com/v-lcc/p/9674975.html

关于日志的123

写在前面: 关于日志其实有很多想说的,不过将自己整理的文档转化为Blog还是比较花时间的,偶有疏漏,请多包涵。 本篇文章所讲均只止于Java。 日志的作用: 1.定位问题,对于一个系统而言,总是会有些…

研究显示每天工作超8小时得心脏病概率增加80%,生命很重要,工作不要那个累。

每天工作超过8小时的人患心脏病的风险最高可增加80%(资料图) 据英国《每日邮报》9月12日报道,芬兰职业保健研究所的科学家们近日进行了一项研究,他们发现每天工作超过8小时的人患心脏病的风险最高可增加80%。 研究人员表示,长时间的工作是许多…

SVN介绍

1.SVN介绍SVN是一个跨平台的开源的版本控制系统,svn版本管理工具管理着随时间改变的各种数据,这些数据放置在一个中央档案库(repository)中,svn会备份并记录每个文件每一次的修改、更新、变动。这样可以把任意一个时间…

记录 Annotation processing is not supported for module cycles.

报错:Error:java: Annotation processing is not supported for module cycles. Please ensure that all modules from cycle [A,B] are excluded from annotation processing 我是想启动两个 maven工程,相互作为服务提供方和消费方,于是在p…

沉淀再出发:Spring的架构理解

沉淀再出发:Spring的架构理解 一、前言 在Spring之前使用的EJB框架太庞大和重量级了,开发成本很高,由此spring应运而生。关于Spring,学过java的人基本上都会慢慢接触到,并且在面试的时候也是经常遇到的,因为这个技术极…

用Python进行机器学习所需环境的配置(转)

源:用Python进行机器学习所需环境的配置

成功创业者所需的能力

1. 富有远见,乐在其中。 如果你能很好地预见自己的公司所在领域在很多年后的样子,这能保证你在该领域取得长久的发展。很多人能在商业领域取得成功并不是因为他们彻底的废旧立新,而是因为他们乘风破浪,能在现有的基础上有所改进和…

记录:non-compatible bean definition of same name and class [com.XXX.XXX]

启动 springBoot 工程时报错: Caused by: org.springframework.context.annotation.ConflictingBeanDefinitionException: Annotation-specified bean name userLogAspect for bean class [com.foreveross.security.config.UserLogAspect] conflicts with existing,…

「日常训练」 Genghis Khan the Conqueror(HDU-4126)

题意 给定\(n\)个点和\(m\)条无向边(\(n\le 3000\)),需要将这\(n\)个点连通。但是有\(Q\)次(\(Q\le 10^4\))等概率的破坏,每次破坏会把\(m\)条边中的某条边的权值增大某个值,求\(Q\)次破坏每次将…

数学家吴文俊批判“中国式奥数”:害人害数学

奥数震动了两位最高科技奖得主 一谈起“奥数”,国内当今数学界的泰斗级人物吴文俊院士就急了。 他在沙发上挺直了腰,瞪大眼睛,伸出手掌指指点点:“是害人的,害数学!” “什么奥林匹克?没这回事&…

CentOS 7 搭建CA认证中心实现https取证

CA认证中心简述CA :CertificateAuthority的缩写,通常翻译成认证权威或者认证中心,主要用途是为用户发放数字证书功能:证书发放、证书更新、证书撤销和证书验证。作用:身份认证,数据的不可否认性端口&#x…

简单明了 - Git 使用超详细教程

见:http://www.admin10000.com/document/5374.html 一:Git是什么? Git是目前世界上最先进的分布式版本控制系统。 二:SVN与Git的最主要的区别? SVN是集中式版本控制系统,版本库是集中放在中央服务器的&…

FileStream功能被禁用

今天还原数据库,遇到如下问题: 网上的解决方法大概是三种: 1、讲数据库备份文件权限设置为“EventOne” 2、打开SQLServer配置管理器,选中服务然后右击“属性”将FileStream相关勾选并重启当前实例服务 3、设置数据库访问级别 USE…

btree索引和hash索引的区别(待更新)

btreehash用于使用 , >, >, <, < 或者 BETWEEN 运算符的列比较。如果 LIKE 的参数是一个没有以通配符起始的常量字符串的话也可以使用这种索引仅仅能满足"","IN"和"<>"查询