上一篇 LdBeth：NuPRL 中的证明 III–我不做metavariable啦 Part I: Atom type 可能有之前用过 Agda 的人会在开始用 NuPRL 以后觉得，没有 inductive type definition，只有 product 和 disjoint union 但是没有区分 data constructor 的类型，好不习慣啊。 其实这个也不是什么大问题，data constructor 可以用 NuPRL 的 Atom 类型来模拟。 Atom 頋名思义就和 lisp 里的 symbol 类似，可以比较相等。 所以一个 inductive data type definition 的 tree data Tree a = Node (Tree a) (Tree a) | Leaf a 可以表示成个 dependent pair ${\bf DEF\ }Tree(a) = rec(T. \Sigma x : {\tt Atom}. {\tt if}\ x =_A {\tt"...
（其实我倒数第三第四章跳了，实在看不动了。。。orz） 初看之下，这本书很逗比：身为一本算法书，只有十多个算法，一半的时间用来定义不知所云的奇葩语言，语言枯燥无比。。。简直什么鬼= = 如果你这样想，只能表明你完全没看进去：就跟Software Foundations是包着Coq皮（想歪的去面壁）的PL书一样，这本书比起纯正的算法书，更算得上是以算法之名，讲PL，讲如何编程，如果你只是来 看算法的话，你一定会失望。如果不是，你来对地方了：读完以后，你会对dijkstra 的The Humble Programmer之类的EWD有着更深的了解，会对computation 改变认识，知道该如何写代码，有一些reasoning/deduction的heuristic，也会感叹于dijkstra疯子般的radical reasoning下，就是不会学到什么算法（除非你算法跟我一样弱得过不去NOIP初赛） 前一半的不知道叫什么的语言已经是一绝了，我看之前完全无法想象跟while大同小异的一门语言能给我带来如此巨大的震撼-formalism跟minimalism尽管不是不可见，但是语言最核心是由nondeterminism construct构建起来的：你有没有考虑过其实你每天用的if语句其实是个败笔？该语言的variable设计也是神来之笔，我一开始看的时候也没明白为什么在极简主义的语言里面要引入如此复杂的东西，认为是画蛇添足，直到一遍又一遍的看，才领悟了精妙之处。。。完爆某另一个图灵奖得主写的算法书里面的不知所云的语言（ 后一半是利用这个语言解决各种问题，比如equivalence class，比如shortest spanning tree。。。一开始他是以极度formal的tone做这个的，proof什么的一个都不漏，到了后期你明白怎么搞了，由于篇幅关系，跳掉了一大部分formal proof，left as exercise，更着重于：我们如何解决这个问题？并给出了一定的example/heuristic，比如对intermediate step做出assumption，（shortest spanning tree中，assume已经决定的set of edge自己也是shortest spanning tree）（换句话说在什么时候需要加强induction hypothesis），比如当你代码钦定了什么的时候，利用之来优化（对一个naive 算法由3 pass改成2 pass，得出Rem’s algorithm），比如把计算从循环中往外拉，改为incrementally update之。。。 这本书其实绝大部分时候都在讲如何去对一个又一个的问题进行分析，分解，最后解决之-一开始的语言设计是如此，后面的算法也是如此，看这本书的过程，更多的像是跟dijkstra一起研究如何解决一个又一个的问题-从问题的定义下手，用直觉更heuristic找出可能有用的insight，并用之分解问题（算法设计），亦或者从现有的方案下手，质疑一切，找出问题，然后精简，或者去掉之（语言设计）。确实，Dijkstra 最后说了大概这样一段话：我们的确不太可能看完一本书，就明白该如何思考，但是我希望你读完这本书以后，能用seperation of concern之类的办法（没错，Dijkstra 发明了seperation of concern，还发明了pair programming，是软件工程中很重要的人（雾）），对一个复杂的问题，进行分解，导致不再复杂，是intellectually manageable的。 不过语言的确很枯燥，英文勉强的不用读了，这更多的我觉得是dijkstra认为“难的东西就是难的，无论如何修饰也是如此”导致的。。。
大家520快乐！祝各位都能跟心仪的另一半进行crossover，产生fitness更高的后代哦~ 蛤？你没有另一半？没关系，本小编发现了一个库，用了这个库，你就能跟心仪的数据结构进行交合了哦~ 更厉害的是，交合对象跟你种类不一样也可以呢。甚至，多p交合也是小事一桩哦~ 你还在等什么，快来implement你内心深处的privateの梦吧！ http://okmij.org/ftp/Haskell/extensible/#crossover Extensible Effect旨在解决一个问题：如何Extensible的添加新Effect（这不废话吗） 我们的老朋友Data Type A La Carte酱尽管对Extensible挺能干的，但在这其实挺苦手的 - DTALC并不能Extensible的改变返回值，而每次新增Effect都需要这样做。 在Generic Crossover中，Oleg用Extensible Effect实现了一个State，一个Coroutine，然后就可以用两个effect来（加上SYB）作任意crossover 圆角骑士魔理沙：一招鲜，吃遍天 里面Session Type作法也很漂亮 - 更准确的说，看OK大法（final tagless，eff）的时候都会觉得像他那样做是正当作法，很trivial/natural，但是往往他本人也要一段时间才找得出来（可以看看eff的前身，当时还依赖奇奇怪怪的Request） 顺带一提，我很喜欢PL的原因是，概念是高度Composable的，新的概念往往可以用毫不相干的旧概念实现 - Generic Crossover用了Eff跟SYB，SYB自身又依赖于Typing Dynamic Typing这种做法，更极端的情况我觉得可以看EK这个comment： https://www.reddit.com/r/haskell/comments/387ex0/are_extensible_effects_a_complete_replacement_for/crt1pzm/ 更具体讲，一半lambda the ultimate一半growing a language呢。 http://library.readscheme.org/page1.html https://www.cs.virginia.edu/~evans/cs655/readings/steele.pdf 另：The Reluctant Heroes莫名的好听 另另：知乎你们搞什么鬼，NLP做得这么烂，默认文章问题有生物学就算了，蔡英文跟马英九什么鬼，好歹要加入用户历史数据作prior啊
题图自如何解读杰洛说的「最短的捷径就是绕远路」？ - 知乎 最近在拜读History of Programming Language，有2K页，累&无聊死了，但有时候很有意思： The American side of the development of Algol - 几天后，Algol 58会议进入僵局 - 某欧洲佬拍桌而起：我永远不会把一个句号当小数点用！ 当晚，Wegstein 提出了一个建议：我们搞三个语言，一个标准语，只有AST，一个交流语，用于把程序写上书里面交流，一个机器语，代码怎么存机器里面是这解决的问题。 哎？这不就是non textual representation of code吗？学过smalltalk/lamdu/MPS，用structural editor的，都知道这个。对于不知道的，可以看看Why Concrete Syntax Doesnt Matter 然而，smalltalk是1972的，比这晚了整整14年，并且59年后（2017），这方法也没成主流。 是什么，使得Algol 58如此超越时代？很简单，因为当时5年后才有ASCII，Algol也是史上第零个有标准的语言。这导致没有一套能关照各硬件的字符集，也没有大量把concrete syntax，language reference弄一起的语言（当时语言就几个），就自然不会让人先入为主的产生‘编程语言就应该定义syntax’。 当然，还有那不知名的欧洲佬对美帝国主义的不妥协。 从这，可以得出一个principle of noncompromise： 一旦妥协，接受局限性，后人就会把局限性视为理所当然。而没有问题，那儿来的答案？跳出盒子思考的最好方式，就是一开始不弄个盒子。 无独有偶，几天前在参加lambdaconf，去听APL，讲师开发了个APL -> C with GPU的编译器，源代码为946行（最短时期750行）跑在GPU上的APL（这项目叫Co-dfns by arcfide）。 猜下是用什么开发的？两个记事本。一个屏幕分两半，左边一个，右边一个。没有scroll bar。代码文件则叫做a, b, c…简直是跟主流开发流程反着来！ 为什么？大体如下： “当我用着最糟糕的工具，有最严苛的字数限制，最没帮助的命名，我明白，代码必须写得最短最清晰，否则记事本的糟糕界面就会让我无法继续。这也是为什么我强烈反对IDE的原因。” 换句话说，这是principle of noncompromise的应用-把问题极端化，让之不得不被解决。 真微妙啊，完全相反的两种syntax处理方式，竟然可以由同一条principle激发出。
最近刚刚看完了Proof and Refutation，好长。。。 讲的是数学界各种对Proof，对Conjecture的看法，很喜欢，不过竟然没有怎么提公理体系，仅仅是一笔带过，这就有点不懂了= = 另：作者好强的文笔，竟然能同时驾驭这么多观点迥异的人物，还能描述他们的发展。。。我然后查了下wiki，好像是个很厉害的人。。。什么时候接着爬下他的work 最后，link： Proofs and Refutations (I) Proofs and Refutations (II) Proofs and Refutations (III) Proofs and Refutations (IV)还有这在CS的应用 Proof-Directed Debugging‘Proof-directed debugging’ revisited for a first-order version 去掉上面的Continuation，更加新手友好 （对于你打算教的人，对你更难了） Proof-Directed Debugging and Repair 试图把Proof-Directed Debugging搞成程序
Abstract：这文章旨意用Coq介绍一下Leibniz Equality，并慢慢引出Curry Howard Isomorphism。 前置知识：Haskell 首先，一些设置： {-# LANGUAGE MonomorphismRestriction, Rank2Types #-} module Main ( main ) where import Prelude hiding(EQ) main :: IO () main = return () 会给出一定的Haskell代码以辅助理解Coq。 Set Implicit Arguments. Set Universe Polymorphism. 第零行开启Coq中的隐式参数。 第一行开启了Universe Polymorphism，详情见Universes，The Coq Proof Assistant，Girard悖论是什么？ - 雾雨魔理沙的回答 - 知乎。不知道这是啥不会影响你的阅读。 当我们认为两个Type相等的时候，我们在说什么？ Monad的创始人（雾，此Monad非彼Monad，不过玄乎程度有过之而不及）Leibniz给出了一个很优雅的解释：当A=B的时候，如果一个命题为真，把里面的任意A替换成B，依然为真。用更formal的话说， Given any x and y, x = y if and only if, given any predicate P, P(x) if and only if P(y). -Equality (mathematics)...
P.S. 这是写给想设计语言的人看的，如果你只是一个用户，不用看了，Syntax的确很重要。 假设你想写一门编程语言。 你想了一会语言大体有什么特性，然后写下一些展示这些特性的示例程序，并且注明它们的输出是啥。 错！绝大部分时候你不应该这样做！你的切入点应该是parser输出的中间结构（多为AST）入手，围绕这东西写各种evaluator/type checker/compiler等，以后再去搞Parser。 0.首先，无论如何，你最初设计的语法都会被你反复修改：注释能不能嵌套？用// /**/ 还是(**)还是#还是;还是;;？tab space有没有意义？def还是define? = 还是 := 还是 :- 还是 <-？这些东西都是互相不兼容的，你就这么多个符号，你选了=做赋值，=？做等价测试，过几天你觉得=?丑想用=做等价测试你就要选另一个东西给赋值。但是如果你是做语言其他方面，就没这么destructive（尽管feature有时候还是会冲突）：你今天写下Type Checking明天写个Compiler后天写GC过几天再写FFI，尽管你写一个东西的时候很可能要去改其他的，但是你是在不停的加东西，而不是单纯的换下一个改上另一个。 难。诚然，你可以手写LL Parser，折腾Parser Combinator，Parser Generator，几十行，大不了100行代码就够了。但是对比一个Simple Evaluator，比如SICP上的eval呢？一个要去折腾各种API，写至少几十行parser，然后再写几十行（很多时候还不到，比如UTLC with HOAS 10行足矣，untyped实现5行就够）Eval，另一个直接从Eval出发，rapid prototyping上讲高下立判。 不必要。除非你的语法真的真的很有特点，（图形化编程界面，APL，这里的标准是一个陌生人看到会不会说一句WTF），不然没有人会仅因你语法漂亮去用你语言。先把大部分精力花在更有意义的东西上，好好折腾有看点的特性，再去考虑语法。 更准确的说，我不是说Syntax不重要-有两种Syntax，Concrete Syntax，Abstract Syntax，Concrete Syntax是你看得见的东西，Abstract Syntax是Evaluator等东西接受的数据结构，举例来说，一个Parser接收Concrete Syntax（绝大部分时候为string）返回Abstract Syntax，然后由Evaluator执行（有的时候Parser直接Eval Concrete Syntax，在这说的不是这种）。Abstract Syntax是很重要的，（比如说Graph/Tree，Binding怎么表达，怎么搞得extensible，支不支持generic programming（见A Generic Abstract Syntax Model for Embedded Languages），是不是homoiconic的，有没有richly typed），搞得不好，自己用着不爽，性能不好，还甚至macro功能打折扣（homoiconicity） 好，你语言折腾得差不多了，其他人有兴趣，想用，（或者你自己开始在里面写很多程序），这时候你可以怎么搞？有一点：别以漂亮的名头把Syntax（含Abstract Syntax）搞的很复杂。或许你自己觉得反正自己只需要写一次，如果其他人用起来爽，就值得了。然而不是这么简单：还有人要去搞Syntax highlighting/Debugger/IDE support/Autocomplete/Static Analyzer这些乱七八糟的东西，搞得太麻烦的话你用户一想起你那麻烦的Syntax就打退堂鼓了（对，复杂如C艹一样这些东西应有尽有，但是C艹是在TIOBE上派前几的语言啊，开发团队，开发出来的受益人群，狂热粉（这些人才可能很抖M地单枪匹马写完整的Parser然后写奇怪的工具）数量都不是你一个没人知道的language能比的） 你也可以机智点，把parser暴露出来，这样写Analyzer/Optimizer的人就不需要自己再写一次了，如果要解放写Editor/Highlighting的人的生产力parser给AST加上奇怪的Annotation估计也可以 还有一个方法：直接不在语言中钦定任何最终用户Concrete Syntax，只钦定一个AST的Format（binary可以XML可以随便搞个Concrete Syntax也恶意）用于保存/交流，然后由各种用户的Editor等去渲染成代码。最好这些工具是可自定义的（或者，由于会有很多工具（比如git上看是一码事，emacs上看是一码事，xxx上看是一码事），这个自定义的东西本身也有一个配置文件标准），这样就从根本上断绝各种Syntax之争：如果你觉得XX更漂亮自己自定义下那些工具就是了，你折腾你的我折腾我的，井水不犯河水。并且这还能玩各种奇奇怪怪的东西：比如说Concrete Syntax没要求是String，这样可以搞Structural Editor/Graphical Editor给喜欢Structural Editing的人/初学者用。 注：456可以一起上 另：其实6在50多年前就提出了。。。历史里面真是有很多有意思的东西。 (The Next 700 PL) Revised Report on the Algorithmic Language Algol 60