Haskell:The craft of functional

書藉基本資料： Haskell:The craft of functional

之前問大中，如果要玩functinoal language，比較推薦那一種？於是大中推薦我看這本學Haskell，浩然只有第一版，只好將就看了。

目前看完Part I Basic Functional Programming，目的是掌握functional language的思維，沒打算實際寫些什麼。2345章順著下來，一章介紹語法，下一章就介紹如何證明程式的性質（reasoning the programs, reasoning the lists），例子淺顯易懂，跟著書裡的範例思考，總算明白證明程式是怎麼一回事。

學PL的人應該會用更嚴僅無誤的方式說明，我針對我的認知說明「證明程式」是怎麼一回事。functional language沒有for, while這些”syntactic sugar”，只有if，剩下的邏輯控制都用遞迴搞定。這樣設計的結果，至少看起來和數學最為接近，程式本身就是數學式子的組合，舉例來說，對函數max(a, b)來說，數學上可以證明max(a, b)有以下的特性：

max(a, b) >= a, for any a max(a, b) >= b, for any b

只要分項討論a >= b和a < b兩個情況，就能證明上面這個性質。換成Haskell的情況，只是用Haskell的語法表示max(a, b)，證明推導的過程就用Haskell的語法表示，而不是數學式子。稍微複雜一點的，可以變成對max(L)，L為一list [A1,A2, A3, …, An]，證明：

max([A1, A2, …, An]) >= max([A1, A2, …, An-1]) >= max([A1, A2, …, An-2]) >= … >= max([A1])

或是

n*max([A1, A2, ..., An]) >= sum_up([A1, A2, ..., An])

其中sum_up(L)表示將list L的內容加總。由於控制流程只有if和遞迴，if 的情況就是分項討論，遞迴可以用數學歸納法。能證明程式性質的話，有機會進一步驗證程式的正確性，比方證明reverse(reverse(L)) = L，或是明白各段程式一定在那些值域內，找出控制語意上的錯誤，像是函數的有效輸入範圍是正數，但輸入的參數值域卻一定是負數。

做為了解程式證明的開始，看這本書頗輕鬆愉快的。