这些东西的优点和弱点仿佛在他心里都有数,他几乎总是指向正确的前进方向。
你知道些什么?可惜的是,由于个人原因,Friedman 始终没有成为我正式的导师(他 “超然物外”,几乎完全不关心自己的学生什么时候能毕业),但他确实是这一生中教会我最多东西的人。所以我想写一些关于他的小故事。也许你能从中看出一个世界级的教育者是什么样子的。我来 IU 之前一位师兄告诉我,Dan Friedman 就像指环王里的甘道夫 (Gandalf),来了之后发现确实很像。
第一次在办公室见到 Friedman 的时候,他对我说:“来,给我讲讲你知道些什么?”我自豪地说:“我在 Cornell 上过研究生的程序语言课,会用 ML 和 Haskell,看过 Paul Graham 的 On Lisp,Peter Norvig 的 Paradigms of Artificial Intelligence Programming, Richard Gabriel 的一些文章……” 他看着我平静地笑了:“不错,你已经有一定基础……”
这么几年以后,我才发现他善良的微笑里面其实隐藏着难以启齿的秘密:当时的我是多么的幼稚。在他的这种循循善诱之下,我才逐渐的明白了,知识的深度是无止境的。他的水平其实远在以上这些人之上,可是出于谦虚,他不能自己把这话说出来。
反向运行Dan Friedman 已经远远超过了退休年龄,却仍然坚持教学。他的本科生程序语言课程 C311 是 IU 的“星级课程”。我最敬佩的,其实是他那孩子般的好奇心和探索精神。几乎每一年的 C311,他都会发明不同的东西来充实课程内容。有时候是一种新的逻辑编程语言 (叫 miniKanren),有时候是些小技巧 (比如把 Scheme 编译成 C 却不会堆栈溢出),等等。
Friedman 研究一个东西的时候总是全身心的投入,执着的热爱。自从开始设计一个叫 miniKanren 的逻辑编程语言,Friedman 多了一句口头禅:“Does it run backwards?”(能反向运行吗?)因为逻辑式的语言(像Prolog)的程序都是能“反向运行”的。普通程序语言写的程序,如果你给它一个输入,它会给你一个输出。但是逻辑式语言很特别,如果你给它一个输出,它可以反过来运行,给你所有可能的输入。但是 Friedman 真的走火入魔了。不管别人在讲什么,经常最后都会被他问一句:“Does it run backwards?”让你哭笑不得。
Friedman 有一个本领域的人都知道的“弱点”——他不喜欢静态类型系统 (static type system)。其实 Scheme 专家们大部分都不喜欢静态类型系统。为此,他深受“类型专家”们的误解甚至鄙视,可是他都从容对待之。
有一次在他的进阶课程 B621 上,他给我们出了一道题:用 Scheme 实现 ML 和 Haskell 所用的 Hindley-Milner 类型系统。这种类型系统的工作原理一般是,输入一个程序,它经过对程序进行类型推导(type inference),输出一个类型。如果程序里有类型错误,它就会报错。由于之前在 Cornell 用 ML 实现过这东西,再加上来到 IU 之后对抽象解释 (abstract interpretation) 的进一步理解,我很快做出了这个东西,而且比在 Cornell 的时候做的还要优雅。
他知道我做出来了,很高兴的样子,让我给全班同学(也就8,9个人)讲我的做法。当我自豪的讲完,他问:“Does it run backwards? 如果我给它一个类型,它能自动生成出符合这个类型的程序来吗?”我愣了,欲哭无泪啊,“不能……”他往沙发靠背上一躺,得意的笑了:“我的系统可以!哈哈!我当年写的那个类型系统比你这个还要短呢。我早就知道这些类型系统怎么做,可我就是不喜欢。哈哈哈哈……”
我后来对类型系统的进一步研究显示,Hindley-Milner 类型系统确实有很多不必要的问题,才导致了他不喜欢。他就是这样一个老顽童。他喜欢先把你捧上天,再把你打下来,让你知道天外有天 :-)
miniCoq你永远想象不到 Dan Friedman 的思维的极限在哪里。当你认为他是一个函数式语言专家的时候,他设计了 miniKanren,一种逻辑式编程语言 (logic programming language),并且写出 《The Reasoned Schemer》这样的书,用于教授逻辑编程。当你认为他不懂类型系统的时候,他开始捣鼓最尖端的 Martin-Löf 类型理论,并且开始设计机器证明系统。而他做这些,完全是出于自己的兴趣。他从来不在乎别人在这个方向已经做到了什么程度,却经常能出乎意料的简化别人的设计。
你知道些什么?可惜的是,由于个人原因,Friedman 始终没有成为我正式的导师(他 “超然物外”,几乎完全不关心自己的学生什么时候能毕业),但他确实是这一生中教会我最多东西的人。所以我想写一些关于他的小故事。也许你能从中看出一个世界级的教育者是什么样子的。我来 IU 之前一位师兄告诉我,Dan Friedman 就像指环王里的甘道夫 (Gandalf),来了之后发现确实很像。
第一次在办公室见到 Friedman 的时候,他对我说:“来,给我讲讲你知道些什么?”我自豪地说:“我在 Cornell 上过研究生的程序语言课,会用 ML 和 Haskell,看过 Paul Graham 的 On Lisp,Peter Norvig 的 Paradigms of Artificial Intelligence Programming, Richard Gabriel 的一些文章……” 他看着我平静地笑了:“不错,你已经有一定基础……”
这么几年以后,我才发现他善良的微笑里面其实隐藏着难以启齿的秘密:当时的我是多么的幼稚。在他的这种循循善诱之下,我才逐渐的明白了,知识的深度是无止境的。他的水平其实远在以上这些人之上,可是出于谦虚,他不能自己把这话说出来。
反向运行Dan Friedman 已经远远超过了退休年龄,却仍然坚持教学。他的本科生程序语言课程 C311 是 IU 的“星级课程”。我最敬佩的,其实是他那孩子般的好奇心和探索精神。几乎每一年的 C311,他都会发明不同的东西来充实课程内容。有时候是一种新的逻辑编程语言 (叫 miniKanren),有时候是些小技巧 (比如把 Scheme 编译成 C 却不会堆栈溢出),等等。
Friedman 研究一个东西的时候总是全身心的投入,执着的热爱。自从开始设计一个叫 miniKanren 的逻辑编程语言,Friedman 多了一句口头禅:“Does it run backwards?”(能反向运行吗?)因为逻辑式的语言(像Prolog)的程序都是能“反向运行”的。普通程序语言写的程序,如果你给它一个输入,它会给你一个输出。但是逻辑式语言很特别,如果你给它一个输出,它可以反过来运行,给你所有可能的输入。但是 Friedman 真的走火入魔了。不管别人在讲什么,经常最后都会被他问一句:“Does it run backwards?”让你哭笑不得。
Friedman 有一个本领域的人都知道的“弱点”——他不喜欢静态类型系统 (static type system)。其实 Scheme 专家们大部分都不喜欢静态类型系统。为此,他深受“类型专家”们的误解甚至鄙视,可是他都从容对待之。
有一次在他的进阶课程 B621 上,他给我们出了一道题:用 Scheme 实现 ML 和 Haskell 所用的 Hindley-Milner 类型系统。这种类型系统的工作原理一般是,输入一个程序,它经过对程序进行类型推导(type inference),输出一个类型。如果程序里有类型错误,它就会报错。由于之前在 Cornell 用 ML 实现过这东西,再加上来到 IU 之后对抽象解释 (abstract interpretation) 的进一步理解,我很快做出了这个东西,而且比在 Cornell 的时候做的还要优雅。
他知道我做出来了,很高兴的样子,让我给全班同学(也就8,9个人)讲我的做法。当我自豪的讲完,他问:“Does it run backwards? 如果我给它一个类型,它能自动生成出符合这个类型的程序来吗?”我愣了,欲哭无泪啊,“不能……”他往沙发靠背上一躺,得意的笑了:“我的系统可以!哈哈!我当年写的那个类型系统比你这个还要短呢。我早就知道这些类型系统怎么做,可我就是不喜欢。哈哈哈哈……”
我后来对类型系统的进一步研究显示,Hindley-Milner 类型系统确实有很多不必要的问题,才导致了他不喜欢。他就是这样一个老顽童。他喜欢先把你捧上天,再把你打下来,让你知道天外有天 :-)
miniCoq你永远想象不到 Dan Friedman 的思维的极限在哪里。当你认为他是一个函数式语言专家的时候,他设计了 miniKanren,一种逻辑式编程语言 (logic programming language),并且写出 《The Reasoned Schemer》这样的书,用于教授逻辑编程。当你认为他不懂类型系统的时候,他开始捣鼓最尖端的 Martin-Löf 类型理论,并且开始设计机器证明系统。而他做这些,完全是出于自己的兴趣。他从来不在乎别人在这个方向已经做到了什么程度,却经常能出乎意料的简化别人的设计。