我想说一些旧闻。更准确的说,我收集了很多旧闻,想整理一下,变成一个没那么旧的旧闻。
0:对于很多编程语言,我们真能做到‘给出编程语言X跟Y,给X一步步加功能,修改下原本的功能,最后成为Y’。我们姑且叫这做计算力吧。这方面的Work数不胜数。
对于Effect,我们有:
C is a purely functional language
Dijkstra Monad(被EK吐槽就是hoare monad on continuation)
Lazy Functional State Thread
Lambda The Ultimate Imperative
Gedanken
对于Subtyping,我们有:
The Essence of Algol(这也应该算Effect的,但那边挤满了)
A Semantics of Multiple Inheritance
至于Type?那就更多了
Untyped Program is unityped program
Gradual Typing上的work,不太清楚
Well typed program cant be blamed
Type System as Macro
Semantic上面有Unified Theory of Programming
编译器上面某种意义上也符合这个样子,如Lambda The Ultimate Goto,Compiling With Continuation,就是在给你说‘你看,函数,高阶函数,其实还是goto那一套。’
当然,LTU Goto严格来说不算Compiler,各种东西都算一点,但不放这一个Compiling With Continuation好孤单(
最后,Prolog也能这样搞,Dijkstra老爷子厉害啊,一个小改动(GCL)竟然能影响到这
1:在PL以外,我们也能做到这点,有的时候还能直接unify出以前还没发现的东西
A Unifying theory of Garbage Collection - 你看看,各种GC算法都是一个路子的
The Periodic Table of Data Structures - 我给你把各种数据结构一家人排得齐齐整整,还给你说你还差啥家人
Demystifying Differentiable Programming - Symbolic Diff = ANF on forward mode, ho reverse mode = CPS fo reverse mode,dual on dual,好漂亮啊
The simple essence of Automatic Differentiation - 跟上面一个样子,Unify各种AD,但是更categorically theoretic
A Discipline of Programming, The Craft of Programming, A Principled Approach to OS,都是教你Stepwise Refinement怎么玩(推算法/写OS),ADOP附加到分布式的伏笔。
A Duality of Sorts,The algebra of programming就是Program Calculation的例子。顺带一提,Program Calculation,Stepwise Refinement,也是刚好对一起啊
Liquid Type,看完给我的感觉就是,I have a Subtyping,I have an Algol W,Uh! Liquid-Type!
Stackless Scala With Free Monads,从Free搞TCO
最后不得不提Lambda the ultimate opcode,直接从某个Lisp Interpreter给你推出CPU wire!如果你问我我最喜欢那篇paper,以我的性格,估计我会看着这篇跟The essence of Algol,最后说出你们都是我的翅膀这种话吧。
另外一提,如何制造SCP018 就是我看完Lambda The Ultimate Opcode,Compiling With Continuation,Stackless Scala With Free Monads,然后想,LTU Opcode能从代码推出wire,我为啥不能反其道而行之,CWC说cont = PC,我就从PC推出cont,再弄出TCO。这操作秀得我自己都好开心,觉得这是最有难度的一篇(其他的收集收集资料谁都能写,就这篇有点original work的样子),然而人民群众不喜欢,正所谓知识越多越反动,orz
差点忘了,CH-XXXXX同构。在这下面我们甚至开始Unify Lazy/Strict了,见Haskell is not not ML。
2:很多时候,我们能发现些Pattern,但我们不知道怎么从一边算到另一边。有的时候甚至不知道怎么用。
CPU其实就是个Interpreter
SuperScalar那就对应Program Analysis
Binary Translation不就是jit吗,我建议大家把x86 cpu加进list of transpiler里面troll JavaScript weenie(((
Types As Abstract Interpretations - 字面意义
Your computer is already a distributed system - 字面意义
Algebra, Algebra, Algebra。。。Algebraic Data Type, The Derivative of Regular Type, Partially-Static Data As Free Extension Of Algebras,还有各种算法里面都会有Algebra
DSL, DSL, DSL everywhere - SQL, ASM, BPF,各个都有安全隐患,需要设计防止(SQL injection, page protection, BPF的整个BPF instruction就是安全措施,不然直接ring0跑用户输入asm就行了啊,还要啥BPF instruction自行车)但是转念一想,这不就是在argue for effect system吗?
3:还有些。。。insight?
同时,这些例子都是Abstraction的极优例子,SQL/ASM抽象得原本领域是啥都不知道。
最后,差点忘了Machine Learning。以前就吐槽过,branch prediction就是mini classifier,想不到真有人用NN去做branch prediction了,maya。这不说,ML对各种连续的任务最近大发神威啊,Learned Index Structure, Auto TVM, Peloton, Data Calculator,Deep Coder,乃至AlphaGo,最近很流行的做法就是用ML去学概率/Cost,剩下的接着上传统方法(读作爆搜)。
一个Recurrent problem是concurrency - Distributed System,Database,Algorithm, OS,Cache Coherent,甚至钻牛角尖点,我们还可以说metastable态也是concurrency issue - tyranny of the clock。然而我们还是没有解决concurrency的方案
4:有时候还发现更多的fundamental incoherency
比如说另一篇我很喜欢的paper就是Miscomputation in software: Learning to live with errors,尽管我早读过了,去看那句‘Pupil Omega: Yo, I tell you, errors are fun! ’还是会被吓一跳。。也许Programming is interface能用stepwise refinement说几句,但是live programming。。。Hazel?圆不过去啊
其实我写这么多,我还是不知道我的中心思想是啥。本文没有中心思想,我也不知道有啥用,我猜我只是想说‘看,我能从一个东西算出另一个,多有趣啊’。也许CHI跟periodic table of datastructure有用,但是剩下的其实都是hindsight。
希望有一天我们能把4/3/2/1都往上移,到最后只剩下0,然后有一天任何一个计算机本科毕业生都能做到‘从继电器开始给你推导出现在的本科CS课程’,那多美妙啊。
Calculemus。如果我漏了啥例子求补充。