Some Pattern on Programming
我想說一些舊聞。更準確的說,我收集了很多舊聞,想整理一下,變成一個沒那麼舊的舊聞。
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?
ofollow,noindex" target="_blank">同時,這些例子都是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。如果我漏了啥例子求補充。