<譯>聲明式編程

原文地址:https://bartoszmilewski.com/2...程序員

這是Bartosz Milewski關於範疇論的博客的第二部分,第一部分已經由 garfileo翻譯完成,建議你們先看第一部分。第一部分導言的地址是 寫給程序員的範疇論

第二部分的導言

在本書的第一部分我曾說範疇論和編程都與可複合性相關。在編程時,你總會不斷地把問題分解到一個你能處理其細節的程度,而後一個個地解決每一個子問題,最後把它們自底向上地從新組合起來。大體來講,這有兩種實現的方法:告訴計算機要作什麼(what to do),或者告訴它如何去作(how to do it)。也就分別是聲明式(編程)和命令式(編程)。編程

你甚至能夠從最底層的地方來理解這件事。複合自己能夠被聲明式地定義,例如hfg的一個複合:segmentfault

h = g . f

或者命令式地定義,這時,先調用f,保留計算結果,再對該結果調用g編程語言

h x = let y = f x
      in g y

一個程序的這種命令式版本一般被描述成按照時間順序執行的一個指令序列。特別是,對g的調用不能發生在f執行完成以前。至少這是一種概念上的想象————不過,在一個參數傳遞方式爲按需調用的惰性語言中,實際的執行順序可能徹底不一樣。ide

實際上,聲明式代碼和命令式代碼的執行過程只會有一點差別,甚至沒有,這取決於編譯器有多聰明。但這兩種方法論畢竟不一樣,尤爲在咱們尋找問題的解決方案時和考慮代碼的可維護性和可調試性時,它們會徹底不一樣。函數

這裏有一個重大問題:當面對一個具體問題時,咱們是否老是能夠在聲明式和命令式的方法中選擇一個?進一步,若是有一個聲明式的的解決方案,是否必定能夠轉化爲計算機代碼?這個問題的答案遠非顯然,而且,若是咱們可以找到這個問題的答案,咱們對宇宙的理解可能就會迎來一場革命。優化

讓我來詳細說說。物理中有一個相似的二元性,它要麼會是一些潛在的深入原則的一個重要部分,要麼會告訴咱們一些有關大腦如何工做的事。理查德·費曼曾經提到,這個對應啓發了他在量子電動力學領域的工做。spa

大部分的物理定律有兩種表達形式。一種使用局部(local)或無窮小(infinitesimal)的思惟。咱們會在一個小鄰域內觀察系統的狀態,而且預測它在下一時刻如何演變。這種想法一般透過一組的微分方程組的形式表達,而且咱們會在一個週期時間裏對它們作積分或求和。翻譯

讓咱們看看這種形式和命令式思惟有多像:咱們經過一系列的「小碎步」達到最終解,而每個碎步取決於前一步的結果。事實上,物理系統的計算機仿真也是循序漸進地把微分方程組重寫爲差分方程組,而後迭代它們。這也是行星遊戲中宇宙飛船的運動方式。在每個時間步長裏,飛船的位置經過一個小的增量改變,它就是速度乘以時間間隔。而速度呢,也是如此迭代計算,它的小增量正比於加速度,也就是力除以質量。調試

asteroids game

牛頓運動定律所對應的微分方程組是有明確寫法的:

F = m dv/dt
v = dx/dt

一樣的方法能夠用來處理更復雜的問題,好比用麥克斯韋方程組來描述電磁場的傳播,或者甚至是用格點量子色動力學來描述一個質子中的夸克和膠子的行爲。

數字計算機的使用促進了這種與時空離散化相結合的局域思惟,史蒂芬·霍夫曼曾試圖將整個宇宙的複雜性約減爲一個元胞自動機系統,這種思惟在這個偉大嘗試中體現到了極致。

另外一種是全局的方法。咱們觀察系統的初始狀態和終止狀態,而後經過最小化某個函數計算出二者之間的軌跡。最簡單的例子就是費馬的最小時間原理。它聲稱光線會沿着時間最小的路徑傳播。特別地,當沒有反射物或折射物時,光線會沿着最短的路徑傳播,也就是一條直線。可是,光在厚實(透明)的材料中會傳播的更慢,好比水或玻璃。因此若是你選擇的起點在空氣中,終點在水裏,那麼光就會在空氣中傳播更長一點以得到水中路線的縮減。這個最小時間所對應的路徑使得光在空氣和水的界面處發生折射,這導出了斯涅爾折射定律:

sin θ_1 / sin θ_2 = v_1 / v_2

其中,v_1是光在空氣中的傳播速度。v_2是光在水中的傳播速度。

和翻譯第一部分的 garfileo同樣,我也遇到了不能在代碼塊中寫下標的問題,同時思否的LaTeX也不能寫行內公式。因而這裏採起了和他同樣的約定方式: _表示下標, ^表示上標。

snell

全部的經典力學(結論)都能從最小做用量原理推出。該做用量就是拉格朗日量沿路徑的積分(對時間),而拉格朗日量則是動能與勢能之差(注意是差而不是和,和是總能量)[所以這個所謂的「做用量」是一個關於路徑的函數,而路徑是一個座標關於時間的函數,因此做用量是一個泛函,而經典力學下粒子的路徑就是這個泛函取最小值的那個路徑。想要更具體瞭解該推導過程,還須要瞭解變分法的相關內容。譯者注]。當你朝一個目標發射一個迫擊炮時,炮彈會先上升,這時重力勢能變大,從而,對做用量積累負向的貢獻。同時炮彈會變慢,在拋物線的頂點達到動能的最小值。而後它會加速以更快地經過接下來的低勢能區域。

圖片描述

費曼地最大貢獻就是意識到了最小做用量原理能夠推廣到量子力學。再一次,這個問題被表達成了已知初始狀態和終止狀態的形式。兩個狀態間的費曼路徑積分被用做計算轉移機率。

圖片描述

咱們的重點是,在描述物理的定律時有一個奇特的難以解釋的二元性。咱們既能夠用局部的觀念,因而萬物都按照一個小增量的序列行進;咱們也能夠用全局的觀念,一旦咱們聲明瞭初始和終止條件,那麼這二者中的過程也就肯定了。

全局的手段也能夠用在編程中,例如在實現射線跟蹤時。咱們聲明(觀察的)眼睛位置和光源位置,須要作的是指出這二者間全部可能的光路。咱們不須要精確的最小化每條射線的飛行時間,咱們會利用斯涅耳定律和反射定律來達到一樣的效果。

局部和全局的手段最大的不一樣就是在於它們對於時空的處理上,尤爲是時間。局部的手段永遠對這裏和當下感興趣,而全局的手段會作一個長程的靜態的觀察,就好像將來早就註定了,咱們只不過實在分析某個永恆的宇宙的屬性罷了。

沒有什麼比用函數式響應式編程(the Functional Reactive Programming, FRP)來實現用戶交互更能說明問題的了。FRP不是針對全部的可能的用戶動做寫一個又一個的獨立的接口,並讓全部人都有那些共享的可變狀態的權限,而是把外部事件看做一個無限長的列表,而後對這個列表作一系列的操做。觀念上來說,這個包含全部將來動做的列表就已經在那兒了,就像程序的輸入數據同樣可使用。一個數字π的列表和一個僞隨機數的列表,又或是一個包含了來自電腦硬件的鼠標位置的列表,在一個程序看來沒有任何不一樣。不管是哪一種狀況,若是你想要得到(列表的)第n項,那你就必須先得到前n-1項。當這個性質用到瞬時事件裏時,咱們就稱之爲因果律

可這和範疇論有什麼必然關係呢?我會說明範疇論契合了一種全局的手段而且所以支持了聲明式編程。首先,不像微積分,範疇論沒有內置的距離或領域的概念,或者時間的概念。咱們有的是抽象的對象和他們之間的抽象的鏈接。若是你能經過一系列的步驟從A獲得B,那麼你只用一步也能夠。此外,範疇論的主要武器是泛構造,而這自己就是全局手段的象徵。咱們已經在實踐中見識過它了,好比,在範疇積的定義中。積定義的方式,就是指明它的性質——一種極其聲明式的手段。積是一個具備兩個投影的對象,而且是最好的那一個——它優化出了某個性質:可以因式化其餘(也知足這種條件的)對象的投影的性質。

productranking

注意把它和費馬的最小時間原理或最小做用量原理比較。

相反,讓咱們把它和更加命令式的傳統的笛卡兒積定義做比較。你在描述如何生成一個積的元素時,會先從一個集合中挑一個元素,再從另外一個集合中挑一個。這是生成一個序對的方式,而後也會有一個拆解序對的方式。

幾乎在每一種編程語言中,包括函數式語言,例如Haskell,積類型、餘積類型和函數類型都是內置的,而不是經過泛構造定義的;即便已經存在一些創造範疇式的編程語言的努力(例如,參見參考文獻中Tatsuya Hagino的論文)

不管是否被直接使用,範疇化的定義支撐了已有的編程結構,而且會引導出一些新的結構。更重要的是,範疇論在聲明式的層面上提供了一種能夠生成計算機程序的元語言。這也鼓勵咱們在實現代碼以前就可以導出問題的範式。

致謝

感謝Gershom Bazerman檢查個人數學和邏輯,和André van Meulebrouck在編輯上的幫助。

參考文獻

  1. The Catsters, Products and Coproducts video.

下一篇:極限與餘極限

相關文章
相關標籤/搜索