Equational Reasoning的含義是什麼？

許多人對Haskell，或pure functional programming language的描述基本上都包括這樣一條優點：有利於進行equational reasoning。

我想知道的是，這個術語是不是字面意義上的「替換」？以及對編程語言設計理論有什麼樣的影響？

@邵成 已經基本回答了，其實主要就是兩個用途，第一個是證明，第二個是優化，如果你想說可以用來計算我也不能說錯，因為你重寫（rewriting）的過程就是計算，按我的理解，計算的本質就是重寫rewriting，從四則運算到微積分，從Lambda演算到圖靈機最開始都定義了一些重寫規則。

如果你想證明：

reverse (reverse xs) = apply (2*n) reverse xs (n &>= 0)


可以在xs上用數學歸納法。在驗證上也比較有意義，也就是說你知道reverse應該有這樣的性質，但是你用QuickCheck的時候卻不成立，那麼顯然你寫的不對。這也側面反映了「純」這一重要的概念在Haskell的體現，假使是OCaml、Scala，裡面有一個變數之類的東西污染了，你就沒法干這件事了。

其次是優化。純函數計算過程有很多可以優化的東西，每種結構都有特有的優化。比如Prelude對map的優化，這裡庫的設計者使用了RULES pragma

map _ [] = []
map f (x:xs) = f x : map f xs

{-# RULES
"map" [~1] forall f xs. map f xs = build (c n -&> foldr (mapFB c f) n xs)
"mapList" [1] forall f. foldr (mapFB (:) f) [] = map f
"mapFB" forall c f g. mapFB (mapFB c f) g = mapFB c (f.g)
#-}


也就是說你用庫的map函數可能會比你自己定義的map函數效率更高。

其中最後一條就是fusion優化。這種優化在Pipe、Conduit里也很常見。

{-# RULES "fuseStream" forall left right.
unstream left =$= unstream right = unstream (fuseStream left right)
#-}


另一個例子九瓜老師博士的課題，CCA（Causal Commutative Arrow），Arrow這種結構上的定律有幾十條，手動優化幾乎不可能，優化Arrow的的確是可以提高很多效率的。優化後的Arrow可讀性差，長度暴增，但是可以通過機器自動做好。九瓜老師在PPT中給出了一個長笛聲音的生成器。

去掉語法糖，完全使用Arrow上的運算表達。把裡邊的一些loop給合起來，變成1個loop以便進一步優化，因為我們有很多代數規則。

也主是說作為程序員只需要寫抽象、很好理解的代碼，把這代碼交給CCA去優化，我們就得到了一個非常快的結果。整個過程中，我們的代碼是簡單、精準、維護的。但是我們必須在Arrow上操作。

就是替換，跟數學上的公理系統下證明命題一樣，通過Haskell的「公理」出發（包括函數抽象/調用、模式匹配和ADT等定義），證明一個等式恆成立。一個簡單的例子（摘自Programming in Haskell）

equational reasoning很重要的一點是在任何context下，證明的等式都是成立的，這一點在非純的函數式語言里很難做到。對編程語言理論的作用我不太清楚，不過至少在編譯優化里，equational reasoning是各種fusion優化的基石。