最近刚刚看完了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搞成程序

You and Your Research如何做research One man’s view of computer scienceCS是啥，可以如何改革（图灵奖得主演讲） 另外膜一下bret victor，推上跟人聊天竟然可以用这个引经据典谈笑风生。。。 On the cruelty of really teaching computing science (EWD 1036) 同样是CS是啥，如何改革教育，我更喜欢这篇，很多很罕见的观点（类比之死，用CS做数学，反智的教育，徒劳无功的‘软件维护’，Characteristica universalis）等等 The Humble Programmer (EWD 340)这也可以看看

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)...

如果大家看过近期的文章，会发现有很多其他人写的文章，比如 @Canto Ostinato 的Stackage 镜像使用说明， @lotuc 的Programming Languages: Application and Interpretation【译6】，@Skillness 的C++模板元编程—lambda表达式简单实现， @品雪 的函数式编程的早期历史， @祖与占 的函数式又是函数式等等。 我认为这些文章都写得挺不错，于是决定开放投稿。 投稿的好处都有啥？你的文章会被更多人看见。 投稿话题偏向于（排在越前越代表同等质量下更大几率接纳）： 0：计算机科学，尤其是编程语言/人工智能相关的 1：数学，最好偏向CS（如离散数学） 2：偶尔会接受点娱乐向的，比如 @Canto Ostinato 的小说，跟车万。。。 如果你在你专栏/你的blog投过稿，你可以把该稿同样投放于此专栏。甚至，你可以在文章内连接自己的**专栏/个人主页，创造回流。 ** 另：如果你短时间内投了大量稿，为了防止刷屏，将会分批处理。 不过如果是1跟2，也请踊跃投稿-我希望专栏文章不要过于单一，如果全部都是haskell的blog的话会很单一的 内容包括但不限于 paper/project/书的广告 技巧/算法/工具/什么鬼的介绍 对啥啥啥的评价

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

Finger Treeshttp://comonad.com/reader/wp-content/uploads/2010/04/Finger-Trees.pdf Finger Trees: A Simple General-purpose Data Structure 最近看了finger tree的一些blog，觉得挺有意思的 可以试下自己对comonad里面的typed 2－3 tree加入插入／del，有一定难度，不过polymorphic recursion就好。。。

【東方】「みこみこ魔理沙」イラスト/相生青唯 [pixiv] abstract：利用Finally Tagless，我们可以把HOAS的变种编译上SKI Combinator，同时保留type safety还有extensibility。 前置知识：HOAS 如果你要写Lambda calculus解释器，你一定会遇到一个问题：如何表示一个binding? 最简单的办法（用string表示variable，substitution就是对所有相等String进行替换）有很大的局限性： data Expr = Var String | Abs String Expr | App Expr Expr deriving (Show, Eq) eval :: Expr -> Expr eval (Var n) = Var n eval (Abs n x) = Abs n (eval x) eval (App l@(Var _) r) = App l (eval r) eval (App l@(App _ _) r) = eval (App (eval l) (eval r)) eval (App (Abs n l) r) = eval (subst l) where subst (Var n') | n == n' = r subst (Var n') | n /= n' = Var n' subst (Abs n' x) | n == n' = Abs n' x subst (Abs n' x) | n /= n' = Abs n' (subst x) subst (App ll lr) = App (subst ll) (subst lr) term = Abs "y" (App (Abs "x" (Abs "y" (Var "x"))) (Var "y")) main = putStr $ show $ eval term 在(\y (\x \y x) y)下做替换，就会成为(\y y)，改变了语义。...

在七树归一（上）里 ，我们成功地找出了同构关系，并且作出证明，最后再对所有东西进行了重构，看似完美结束了．然而要玩，还是有地方能重构的． 比如说，我们的核心定义， Definition Combine_helper (T1 T2 T3 T4 T5 T6 T7 : Tree) : Tree := match (T1, T2, T3, T4) with | (Empty, Empty, Empty, Empty) => match T5 with | Node T5a T5b => [[[[Empty, T7], T6], T5a], T5b] | Empty => match T6 with | Node _ _ => [[[[[T6, T7], Empty], Empty], Empty], Empty] | Empty => match T7 with | [[[[T7a, T7b], T7c], T7d], T7e] => [[[[[Empty, T7a], T7b], T7c], T7d], T7e] | _ => T7 end end end | _ => [[[[[[T7, T6], T5], T4], T3], T2], T1] end....

众所周之，一颗二叉树的定义是： 空的，或 一个元素，加上两颗二叉树树（一个结点） Inductive Tree T := | Empty | Node : Tree T -> T -> Tree T -> Tree T. T可以是任何东西，比如说自然数，链表，字符串，另一个Tree等等．．． 那T可不可以是unit，不带有任何信息？换句话说，可不可能T的所有元素皆相等于一个常数？在此之下，Tree有没有意义？ Inductive Tree := | Empty | Node : Tree -> Tree -> Tree. 当然可以！那没，既然树没有保留任何关于元素的信息，有什么意义？ 尽管树不保存元素，就如同list unit并不是毫无意义，而是跟自然数同构一样，树自身的结构已经保留了一定的信息． 那这棵树有什么特别的地方吗？他跟一个结构有着很简单的同构关系（一一映射）． 跟他自己．不，跟7个他自己 ．换句话说，Tree~=Tree^7． 具体证明在Seven Trees in One at Steven Landsburg ，我们今天要试着把这个用Coq证明一遍． 我们先给出一个简写： Notation "[ a , b ]" := (Node a b). Notation "0" := Empty. 这里是把七棵树合并的定义： Definition Combine_helper (T1 T2 T3 T4 T5 T6 T7 : Tree) : Tree := match (T1, T2, T3, T4) with | (Empty, Empty, Empty, Empty) => match T5 with | Node T5a T5b => [[[[Empty, T7], T6], T5a], T5b] | Empty => match T6 with | Node _ _ => [[[[[T6, T7], Empty], Empty], Empty], Empty] | Empty => match T7 with | [[[[T7a, T7b], T7c], T7d], T7e] => [[[[[Empty, T7a], T7b], T7c], T7d], T7e] | _ => T7 end end end | _ => [[[[[[T7, T6], T5], T4], T3], T2], T1] end....