IFIP Working Group 2.1 Meeting #65

IFIP Working Group 2.1 第 65 次集會的「正式」決議:

The members of WG2.1 and the observers present at the 65th meeting in Póvoa de Lanhoso, Braga, Portugal, wish to thank José Nuno Oliveira, João Saraiva, Luis Barbosa and Sara Fernandes from the University of Minho for a meeting that was warm, refreshing and enlightening.

In fact, from a study of the superlative room temperatures of the meeting room and the coffee room we determined a connection that can precisely and concisely be summarized as

    C ⊢ M.

A little reflection led to glear galculations that dispelled glouds of obsgurity. After digesting what we were presented with, we ended the week at maximum density.

留作紀念。

Posted in 未分類 | Leave a comment

找出該證的性質,然後證明它

研究所入學那天,老師照例勉勵新生們。多年後,除了指導老師說的一些事,我只記得這麼一段話:「所謂做研究,就是找個好問題,然後解決它。前者通常比後者難。

很遺憾,剛到所上誰都不認識的我竟不記得是誰下了這麼一個雋永深刻的評語。

過去兩週試著證明一個演算法的正確性,本希望能在一週內解決,硬是拖了一倍的時間。這時回想起那句話,倒是在小尺度內有了類似的感觸:做我們這種研究,就是找出那個該證的性質,然後證明它。前者通常比後者難。

所謂一個演算法「正確」,指的是其算出的東西符合規格。這當然是我們最後希望證明的性質。但通常這無法直接證。我們得證明該演算法滿足某些不變量 (invariant). 理想上,不變量在設計演算法時就該推導出來。實際上,我們常得要證明別人的演算法,而對方對不變量只有一個籠統模糊的描述;或著我們討論的是還在成形中的演算法。這時只好猜。

於是我們靠感覺和經驗猜:整個演算法如果有效,某個性質要應該成立吧。理想情況是立刻用一個歸納證明漂亮搞定。實際上,一個大定理通常無法整塊一口氣證出來,得拆成幾個輔助定理。怎麼拆呢?照經驗,並靠著對問題的了解。嗯,也許它會對,是因為這個、這個、和那個。拆成三個小性質,把最明顯、應該不會不成立的擱一旁,從問題較大的開始證。

那麼,開始歸納證明囉?硬推幾步後常會發現這樣行不通。為了歸納證明,我們得證一個更廣泛、更強的性質。廣泛化的方法很多種,要挑哪個?只好再靠經驗猜了。這是一個不斷調整的過程:你證的性質得強到可提供足夠的歸納假設,又不至於過強到證不出來。總之,分出幾個 case,推了幾步之後,開始三心二意了。這樣對嗎?

往往事情就是愛捉弄人。好不容易證完第一個補助定理、第二個補助定理,再回頭看當初擱一邊的、覺得很明顯應該會對的那個補助定理,其實是錯的。

啊,只好再重新開始了。追根究底,那是因為我們還不夠了解手上的問題。要正確地把性質切成小塊,我們得對問題有全盤的了解。但全盤的了解又根基於從每個細節的運作中學到的經驗。而人腦能同時處理的問題複雜度有限,於是只好反覆東想、西想,不知該由上往下、還是由下往上?

用 Coq, Agda 之類的證明輔助程式可能讓情況更糟糕。我原以為電腦適合證明有很多 case 的性質,因此把定理放到 Coq 或 Agda 裡,希望靠著問答和填空格就可以糊裡糊塗地把性質證出來。結果我得到的慘痛教訓是:若不先想清楚,證明輔助程式剛好賦予你在錯誤的路上走得更遠的能力。我寫了幾百行的證明,迷失在許多細節裡,才發現此路不通。也許證明還是得先在紙上做一遍吧?

等到終於找到那組對的性質,也終於確定把這問題搞懂了。證明可能不過是十幾分鐘的事情。「就這樣?」這很明顯嘛。怎麼沒早點想通呢?

這就是做我們這行研究呀。

Posted in 未分類 | 7 Comments

資訊學研究成果的評估

怎麼評估資訊科學學者或系所的學術成就?別的學科都在衝 SCI 論文數的同時,資訊科學家得不斷費脣舌解釋對圈內人來說,頂尖的會議和頂尖的期刊一樣重要、出書也是重要的貢獻、做出一套軟硬體工具造成的衝擊可能比論文大很多…。何建明老師發現了國科會簡訊網不同學門領域對於學術發表的態度--德國觀點系列4:資訊學一文,翻譯宏博基金會資訊學領域審查員 Franz J. Ramming 的文章,對於資訊科學界的實況有清楚的描述,適合一讀,也方便拿給別人看。結論:

  • 資訊學領域對會議和期刊的評價是同等的。
  • 學術會議和期刊都採取一個嚴格的「同儕審查制度」。
  • 會議論文以完整篇幅刊登於會議論文集。
  • 會議和期刊的排名相當困難。因此資訊學界必須聽取各審查人的評估意見。
  • 如果一項會議辦得非常成功,這通常顯示主辦單位具有高度學術品質。
  • 資訊學界比較注重專門學科的會議或專門期刊,幾乎沒有出版單位從事廣泛方面的出版。
  • 多人同著一書或一文時,作者列名方式以其對該發表文章或書籍的貢獻程度而定。
  • 基於主任身份而自動被列爲作者的現象在資訊學仍不屬慣例,但是很遺憾的是這個現象越來越常見。
  • 資訊學人相當早就開始發表,通常在碩士階段就撰文投稿。
  • 資訊學深受美國影響,各地區的特色並不顯著。
  • 資訊學是非常多樣化的,本文所敍述的一般慣例只是粗略的概述而已。

該文談到 ACM, IEEE CS 的角色,也點出「亞洲地區和其他地區越來越明顯的現象是出版機構的國家(國內)排名。這造成遴選教授候選人時,只認定某些特定機構的出版物作爲審核的範疇。」

另一個值得注意的現象是「亞洲地區…與外隔絕。我們可以假設語言障礙是造成這個現象的主要原因。」「新興國家和發展中國家… 的年輕學者幾乎毫無機會參加國際學術會議。資訊學是一個非常注重學術會議的領域,這麽一來,那些國家在發展資訊學領域就遭遇很大的困難。… 沒機會參加國際會議,就無法打出自己的知名度。這些年輕學者如果沒有機會受教於一位國際知名學者的話,只好參與地方性的會議或向當地期刊投稿。」對台灣來說,我不知這樣的情形有多嚴重。大家認為呢?

Posted in 未分類 | Leave a comment

泛型與索引編程春季班

今年三月,EPSRC 補助的泛型與索引編程計畫將在牛津大學開設五天的課程: Spring School on Generic and Indexed Programming,講者包括:

  • Nate Foster (Princeton University): Bidirectional Programming
  • Ralf Hinze (University of Oxford): Generic Programming with Adjunctions
  • Oleg Kiselyov (Fleet Numerical Meteorology and Oceanography Center): Typed Tagless Interpreters
  • Simon Peyton Jones (Microsoft Research Cambridge): Type Functions
  • Jeremy Siek (University of Colorado at Boulder): Concepts in C++
  • Stephanie Weirich (University of Pennsylvania): Generic Programming with Dependent Types

詳情請參閱公式網頁

「泛型編程 (generic programming)」這詞大家可能較常看到。如同網頁上說的,泛型編程的目標是讓同一段程式能用在更多種不同的情況。諸如資料的形狀、代數結構、演算策略等都可以成為程式的參數。函數編程圈內談得較多的是資料型別的泛型 — 讓同一個函數可以用在串列、二元樹、多元樹等不同資料結構上。這和物件導向圈內的「泛型」稍有不同,但兩邊的人一直試著溝通、了解彼此的語言。

用依值型別 (dependent type) 來作泛型編程是最近的一個新嘗試。所謂索引編程 (indexed programming) 是一種較輕量的依值型別應用,我不知怎麼翻譯比較合適。

這次講師陣容蠻堅強的,牛津也是個好地方。有可能的話很推薦大家去。

Posted in 未分類 | Leave a comment

Algol 60 五十週年紀念

1960 年一月 1 日至 16 日,歐洲與美國的計算科學家在巴黎開會制定了影響深遠的程式語言 Algol 60。本月 14 日,英國電腦學會(BCS) 高等編程組電腦保育學會將舉辦一日討論會:50 years of Advanced Programming – an Anniversary Seminar on Algol 60,紀念 ALGOL 60 報告 50 週年。議程如下:

  • Mike Woodger interviewed by Brian Wichmann
  • Brian Randell on "Early compilers"
  • Cliff Jones with a contribution from Tony Hoare
  • Richard Bornat on Peter Landin’s early work
  • Cliff Jones with a contribution from Luca Cardelli
  • David Holdsworth speaking on revivifying the KDF9 compiler
  • Peter Onion speaking on practical aspects of using the Elliott 803 compiler

會期主席為 John Florentin and David Hartley。靠近倫敦的朋友可以去看看!

Posted in 未分類 | Leave a comment

為何 SCI 論文數不適合評鑑資訊科學

大學評鑑排名是國內前一兩個月的熱門話題。在學術成就評量這項目中, 被 Thomson ISI 公司的 SCI, SSCI 等資料庫收錄的論文數量佔很重比例,於是 SCI 論文數也跟著被當作個人學術成就或對系所「貢獻度」的量化指標。學者們對這套量化思維多少有不滿,但國內電腦科學(資訊工程、資訊科學等)學界出聲的似乎還不多。最近朋友告知 Friedemann Mattern 的一場演講以及一份歐洲資訊研究評鑑委員會 (Research Evaluation Committee of Informatics Europe) 的報告(以下簡稱為 RECIE),說到 SCI 其實特別不適合資訊科學/電腦科學。此處摘錄一些重點和心得。

論文數量或被引用數量到底是不是可信認的評量指標本就是個有爭議性的問題。但我們姑且先不談到這層面,光看「數論文數目」這差事,ISI 到底有沒有做好?

幾個邏輯推論:首先,SCI 資料庫若可當作評鑑標準,資料庫內的論文至少應滿足 ISI 和評鑑單位認定為好的、重要的、上得了檯面的最低條件。1 其次,合理情況下,一篇論文應不致於引用很多比自己差太多的文獻 — 雖然偶有引用一篇論文並指出其錯誤的情形,畢竟只佔部份。所以 SCI 資料庫內的論文所引用的文獻大部份也應滿足被收錄的標準才對。對生物領域論文來說,「被引用的文獻也出現在資料庫內」的比率是 90%,物理和化學也都超過 80%. 總有論文會引用一些技術報告、私人通訊等等,這個比率自然不可能達到百分之百。

但電腦科學呢?竟只有 40%! 如果再加上 ACM, IEEE-CS, LNCS 等論文,勉強可以達到 51%. 也就是說一篇電腦科學 SCI 論文所引用的文獻平均將近一半是不在 SCI 資料庫中的。若不是電腦科學家引用的習慣超出常識想像,就是 ISI 遺漏了很大比率的文獻。一個缺了一半文章的資料庫已經很難當作評鑑標準。

有人會說這是因為 SCI 以索引期刊為主,而電腦科學界的特殊現象之一是許多好論文只投給會議。學界的習慣到底好不好可再另外討論,但重點是一個評鑑標準本就應該反映實況,「學術貢獻」評鑑應反映出圈內學者所認可的貢獻。況且,ISI 的情況遠比「期刊 vs 會議」來得複雜,基本問題是 ISI 心目中的電腦科學和我們的理解大不相同。RECIE 報告中提及,ISI 的「最常被引用期刊」前 50 名包括 "Chemometrics in food science" (第 13 名)等大部分電腦科學家沒聽過的期刊。而這並不是特例。ISI 排名第一的期刊在 CiteSeer 排名 195;CiteSeer 的第一名在 ISI 排名 26. (雖然這類資料庫不可能完美,但 CiteSeer 的名單至少看來熟悉許多。)比較 ISI 和 CiteSeer 的最常引用文獻,兩者居然連一個共同項目都沒有。有人把這當作此類排名通通不可靠的證據,但 ISI 顯然對電腦科學界相當不了解。

ISI 的「最常被引用學者」中並沒有 Wirth, Parnas, Knuth 等人。2000 到 2006 的 Turing 獎得主中只有 Ronald Rivest (RSA 演算法中的 R) 上榜。但不包括 Adi Shamir (RSA 中的 S)。

因此 Mattern 說,ISI 眼中的電腦科學和學界的實況根本就是「兩個世界。」

ISI 最近把 Springer 的 LNCS 系列算為期刊,雖然該系列大多是會議論文集和專題論文。2而許多不經由 LNCS 發表論文集的會議仍未被索引。因此 International Conference on Software Engineering,軟體工程學界最好的會議之一,並沒有被索引。但一個被 LNCS 出版的工作坊會議卻可以算成 SCI 論文,即使圈內人都知道這個工作坊大都是在投稿 ICSE 之前先試試水溫用的。

ACM 程式語言組的 SIGPLAN Notices 也被 ISI 索引。事實上,SIGPLAN Notices 是一個收錄筆記與草稿、沒有同儕審核的刊物。但每逢大型會議,SIGPLAN Notices 也會出版包括 POPL, PLDI 等高水準會議的專刊。專刊和一般期數的意義大不相同,ISI 把它們視作一樣的文獻。

其他評鑑標準?

Mattern 的演講與 RECIE 報告並不只談 ISI 的問題。其他的量化指標也有各自的缺點。另一個資料庫 SCOPUS 的最常引用文章全都以應用領域 ( "computational X") 為主;而像 CiteSeer, Google Scholar 等工具則有電腦判斷失誤的問題。後兩者的好處是錯誤訂正的機制較透明。3

電腦科學界有些獨有的特性:除了期刊,書和會議也很重要(若問人電腦科學最重要的著作是什麼,很多人會回答 The Art of Computer Programming);成功的硬軟體實作影響力可能遠超過論文;論文共同作者數目介於自然科學與數學之間,作者排名順序較不重要;4 有許多子領域,之間交互引用的情況不多;有競爭相當激烈、被引用數很高的會議,也有更多幾乎沒有被引用過的會議。這使得對電腦科學的評鑑應有個不同的設計。

當然,我們終究得談到,被引用數目是個公允的影響力指標嗎?(調查、介紹性的論文被引用量會比較高;第一個提出 NP Complete 概念的論文被引用數遠不及後來的闡述者… )這類量化指標的問題在哪?但這些已屬學界各領域都會碰到的問題了。

Mattern 任職於瑞士 ETH, 電腦科學的著名研究重鎮。但從種種指標看來,ETH 好像並沒有什麼重要的電腦科學研究似的。ETH 的「每人被引用數」排名是如何從 2004 年的第三名掉到 2005 年的 71 名,只因為計算方式改變了?想知道詳情,我很推薦大家看看他的投影片。

對於 SCI/SSCI 當作評鑑指標,國內人文學界的反彈似乎強過科學與工程。也有人認為這是一種缺乏自信的表現、台灣/華人/亞洲特有的現象(例如把 SCI 稱為 Stupid Chinese Idea 等等)。但歐洲也有人談及此事,大概他們也覺得受夠了。國外學者指出 SCI 其實特別不適合電腦科學,國內資訊科學界的看法又是什麼呢?

附註

  1. 之所以說是「最低」條件,因為 SCI 資料庫原為一個檢索與分析為目的的「完整」資料庫,被索引的期刊自應是有好有壞,僅被列名並不足以視為「好論文。」我們為主事者硬找個用 SCI 資料庫當評鑑的合理邏輯,只能說主事者大概認為 SCI 資料庫裡有的東西「至少可以算是論文。」意即 SCI 被當成一個「正式論文」發表量,而不見得是「好論文」發表量。但如此一來 SCI 資料庫的涵蓋範圍就應更廣。
  2. 2009/11/19 update: RECIE 報告草稿日期為 2008 年五月,但 LNCS 在 2006 年之後就不收錄於 ISI, 而改收錄到 ISI Proceedings List 中。該報告指的可能是 2006 年之前的論文。
  3. 所內最近和愛因斯坦成為共同作者的某 A 小姐可能並不會很想去訂正就是了。
  4. Nature 一年的樣本中平均每篇作者 7.3 人,最高 22 人;American Mathematical Monthly 平均兩人,最高 6 人;OOPSLA 與 POPL 平均 2.7,最高 7 人。

參考資料

  1. Friedemann Mattern. Bibliometric Evaluation of Computer Science – Problems and Pitfalls. European Computer Science Summit 2008.
  2. Research Evaluation for Computer Science. An Informatics Europe report

參考連結

Posted in 未分類 | 4 Comments

單子 (monad) 入門(二)讀取單子

為了進入下一個例子,我們為算式型別加上變數:

data Expr = Num Int | Neg Expr | Add Expr Expr
          | Var Name | Let Var Expr Expr

Name 是變數名稱。我們可以用 type Name = String 或著其他型別,只要能夠比較兩個變數是否相等就可以了。Var v 是出現在算式中的變數,Let 則用來宣告新的區域變數。例如:

Let "x" (Num 3) (Add (Var "x") (Num 4))

宣告變數 x 的值為 3, 因此整個算式的值是 3 + 4 = 7.

變數與環境

有了變數後,我們不能只問「Add (Var "x") (Var "y") 的值是什麼」了。有自由變數的算式得放在一個「環境」下才能談它的值。「環境」告訴我們每個變數的值,用行話說,環境是從變數到值的映射,我們可以用一個串列表示:1

type Env = [(Name, Int)]

例如 Add (Var "x") (Num 4) 在環境 [("x", 3), ("y", 6)] 下的值是 7. 我們也假設有一個「查表」函數:

lookup :: Env -> Maybe Int

例如,當 env = [("x", 3), ("y", 6)]lookup env "x" Just 3lookup env "z" 則是 Nothing.

有點得注意:雖然我們照習慣把 x 稱為區域「變數」 (local variable),x 的值一但給定了就不會改變。例如這個式子的值

Let "x" (Num 3)
    (Add (Add "x" (Let "x" (Num 4) (Var "x")))
         (Neg (Var "x")))

應該是 3 + 4 + (-3) — 內層宣告的 x 僅是暫時遮蓋到外面的 x。這和我們之後會提到的、一般指令語言中的設值運算 (assignment) 是不同的。

這麼多鋪陳之後,我們終於可以看看新的 eval 函數要怎麼寫了。我們待會兒會介紹讀取單子 (reader monad), 但顧及有些讀者可能還不習慣這樣的運算,我們先把單子放一邊,看看怎麼用最直接的方式寫 eval.

既然算式要在環境之下才有值,eval 得把環境也納為參數之一:

eval :: Expr -> Env -> Int

函數 eval 拿一個算式和一個環境,計算該算式的值。新的 eval 中,最初的三個條款基本上是一樣的,只是多了一個參數 env 得往下傳:

eval (Num n) env = n
eval (Neg e) env = - (eval e env)
eval (Add e1 e2) env = eval e1 env + eval e2 env

碰到變數時,我們到環境中查變數的值:

eval (Var x) env = case lookup env x of Just v -> v

這裡的 case 算式只處理了 Just 的情形。如果 lookup 傳回的是 Nothing,也就是變數 x 並不在環境 env 中,該怎麼辦呢? 我們等下再談。最後,碰到 Let x e1 e2 時,我們先把 e1 的值在 env 這個環境之下算出,然後算 e2:

eval (Let x e1 e2) env =
  let v = eval e1 env
  in eval e2 ((x, v) : env)

但計算 e2 時必須使用新的環境 (x, v) : env,意謂 e2 可以用到 x, 而 x 的值是 v.

算式的語意是函數

回到單子。在單子入門(一)中,單子版的 eval 是這樣寫的:

eval :: Monad m => Expr -> m Int
eval (Num n) = return n
eval (Neg e) = eval e >>= (\v -> return (-v))
eval (Add e1 e2) = eval e1 >>= \v1 ->
                   eval e2 >>= \v2 ->
                   return (v1 + v2)

我們也提及了,單子讓我們模組化地加入新功能。我們要怎麼以這個程式為基底,靠著選用不同的單子,把「處理環境的功能」加上去呢?

函數 eval 沒有副作用時的型別是 Expr -> Int — 一個算式的「意思」就是一個整數。加上變數、考慮環境的 eval 的型別變成了 Expr -> Env -> Int. 一種讀解方式是:eval 拿一個算式,傳回一個函數。也就是說,一個算式的「意思」(用行話說,是算式的語意)成了「拿一個環境,傳回一個整數」的函數。的確,既然算式算成的那個整數必須由環境決定,算式其實不能看作一個數值,而應該是從環境到整數的函數才對。eval (Add (Var "x") (Var "y")) 是一個函數,如果給它 [("x", 3), ("y", 2)], 我們得到 5. 如果給 [("x",4), ("y", -3)], 我們得到 1.

如果我們把這個「從環境到整數的函數」叫做 Reader a, 也就是說定義 type Reader a = Env -> a,函數 eval 的型別成了 Expr -> Reader a. 我們能不能讓 Reader a 成為一個單子呢,也就是說,定義符合單子定律,並也符合我們需求的 return>>= 兩個運算元呢?

讀取單子

回顧一下 return>>= 的型別:

return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b

此處 m a = Reader a = Env -> a. 讀取單子的 return 定義是

return x = \env -> x

意即 return x 不產生副作用、僅傳回純數值 x. 環境 env 並沒有用到。回顧一下兩個版本的 eval 如何處理 Num:

原始版: eval (Num n) env = n
單子版: eval (Num n) = return n

確實後者代入 return 的定義後就成了前者。

>>= 的定義是:

r >>= f = \env -> f (r env) env

此處 r 的型別是 Env -> a, f 的型別是 a -> (Env -> b). 等號右手邊是一個函數, 拿了一個環境 envr 需要一個環境才能算出一個 a,因此我們把 env 餵給它。算出的結果送給 f. 但 f (r env) 又是一個讀取單子,仍需要一個環境才能算出 b. 因此我們把同一個環境 env 又餵給它一次。

環境 env 是被兩個運算共用的。這可解釋為何我們把 eval 的 Add 條款

eval (Add e1 e2) = eval e1 >>= (\v1 ->
                   eval e2 >>= (\v2 ->
                   return (v1 + v2)))

展開後,會得到 eval e1 env + eval e2 env. 我們仔細看看讀取單子在此如何運作:整個等號右手邊是個拿一個環境的函數。根據 >>= 的定義,環境會丟給 eval e1,算出的值交給 >>= 右邊的函數 (\v1 -> ...)。因此右手邊成了:

\env -> (eval e2 >>= (\v2 ->
         return (eval e1 env + v2)) env

內層的 eval e2 >>= ... 也用同樣的原則化簡:它也是期待一個環境的函數,剛好把外面的 env 接受。化簡後得到

\env -> return (eval e1 env + eval e2 env) env

最後把 return 展開就成了 eval e1 env + eval e2 env.

Ask 與 Local

我們還得加上處理 VarLet 兩個情況的條款。遇到 Var x 時我們得到環境中查詢的值。原有的寫法是:

eval (Var x) env = case lookup env x of Just v -> v

此處這麼寫也是可以的。但標準的讀取單子定義中提供了一個函數 ask, 方便我們把環境給取出來用:

eval (Var x) = ask >>= \env ->
               case lookup env of Just v -> v

函數 ask 可定義為:

ask :: Reader Env
ask env = env

也就是說 ask 拿到一個環境後直接傳回該環境。

而處理 Let x e1 e2 的條款需在擴充過的環境中求 e2 的值。。為了這類的需求,標準讀取單子也提供了一個方法:

local :: (Env -> Env) -> Reader a -> Reader a
local f r = \env -> r (f env)

其中 f 是產生新環境用的函數。local f r拿到一個環境 env,但在環境 f env 中執行 r. 函數 evalLet 條款便可寫成

eval (Let x e1 e2) =
    eval e1 >>= \v1 ->
    local (\env -> (x,v1) : env) (eval e1)

意義很清楚:先算出 e1 的值,稱作 v1, 而 e2 的值須在區域環境 (x,v1) : env 中計算。其中 \env -> (x,v1) : env 還可稍微簡寫一下:

eval (Let x e1 e2) =
    eval e1 >>= \v1 ->
    local ((x,v1) : ) (eval e1) 

討論

結束本文前,我們再提幾件事情。

首先,上述討論中為了說明方便,假設環境的型別固定為 Env. 我們當然可以把這部份也抽象掉:

type Reader e a = e -> a 

return, >>=, ask, local 的型別也隨之改變,但其定義原就沒有預設環境的型別,仍可沿用。

其次,如同單子入門(一)中的單位單子一樣,如果要使用 type class, Haskell 要求我們必須把 Reader 定義成一個新資料型別(type 定義的僅是別名)。目前標準函示庫中的定義請見附錄。

最後,我們稍早曾遇到這個問題:如果給這樣的式子

eval (Var "x") [("y",0)]

變數 "x" 並不在環境中,lookup 將傳回 Nothing,這時該怎麼辦?

我們可以再擴充 Reader 的型別,讓 eval 也可以傳回一個 Maybe 結果:

type ReaderMaybe a = Env -> Maybe a

return>>= 也得隨之擴充:

return a = \env -> Just a
rm >>= f = \env -> case rm env of
                    Just v -> f v env
                    Nothing -> Nothing

這個 ReaderMaybe 型別綜合了讀取單子與 Maybe 單子的功能,其 return>>= 定義也像是兩個單子定義的混合。它也是一個 MonadPlus, eval 在碰到上述情況可以傳回 mzero. 這時 mzero 的定義應該是 \env -> Nothing.

但這並不是令人相當滿意的做法。ReaderMaybe 比起 Reader 又更複雜了一點。日後我們也許會想要有更多功能,例如狀態、輸出入等。ReaderMaybe 已經夠抽象難解了,我們並不希望設計、維護越來越龐大的單子。

既然 Maybe 單子讓一個程式加上「例外」的副作用,讀取單子讓一個程式加上可存取環境的功能,我們能否把這兩項功能分別模組化地加入呢?

也就是說,給了兩個單子 M1 和 M2, 能否把他們的功能加在一起,產生另一個新單子呢?

這曾經是困擾函數編程學者的難題,直到出現了「單子轉換器 (monad transformer)」為止。以後我們希望能談到。

下次我們會繼續介紹另一個有用的單子 — 狀態單子。

附註

  1. 其實既然環境是一個映射,我們用的又是函數語言,更方便的做法是用函數表示環境:
    type Env = Name -> Maybe Int

    為了避免不習慣高次函數的初學者搞到困惑,本文還是用比較「摸得到」的串列表示 Env.

附錄:以 newtype 定義的讀取單子

newtype Reader e a = Reader { runReader :: (e -> a) }

instance Monad (Reader e) where
    return a         = Reader $ \e -> a
    (Reader r) >>= f = Reader $ \e -> f (r e) e 

class MonadReader e m | m -> e where
    ask   :: m e
    local :: (e -> e) -> m a -> m a 

instance MonadReader (Reader e) where
    ask       = Reader id
    local f c = Reader $ \e -> runReader c (f e) 

Posted in 未分類 | 10 Comments

程式設計的公設基礎:四十年後

1969 年,C.A.R. Hoare 在 Communication of the ACM (12(10):576–580) 發表論文 An Axiomatic Basis for Computer Programming,在文中提出後來被稱作 Hoare 邏輯 (Hoare Logic) 的一套公設系統, 被認為是計算科學史上最重要的幾篇論文之一。時間轉眼間過去了,今年已經是這篇論文的四十歲生日。最近 Hoare 應 Communications 之邀,回顧後來的發展。有哪些是他預期的,哪些是他沒料到的?

1960-68 年間,Hoare 仍在業界工作,帶領一個實作 ALGOL 60 編譯器的團隊。ALGOL 的語法用 context-free language 定義得相當精簡優雅,語意卻仍以非形式的方式定義。Hoare 希望有個方式能一方面嚴格描述 ALGOL 的語意,一方面又不限制到編譯器製作者使用各種最佳化方法的自由。這是 Hoare 邏輯的由來。

Hoare 漸漸發現這題目大概可以研究一輩子。而且大概直到他退休,這東西也不會在業界得到廣泛應用。這使他在 1968 年從業界進入學界,而到他 1999 年退休為止,看來這兩個預測都蠻準確的。

令他意外的事情呢?Hoare 說他可以預期程式會越來越大,測試這種大程式也會越來越困難。他沒想到的是測試不僅是用在程式上,更是對人的考驗。通過這種考驗的工程師所培養出的直覺和經驗也是讓軟體可靠的重要因素。形式方法應該去支持程式員的直覺判斷,而非壓抑它。況且開發中的軟體若在測試中表現得很差,剛好可讓開發部門作為說服管理部門延長開發時間的依據。

把測試和證明對立起來的看法也許是個基本錯誤 — 工程師本來就要使用各種有用的工具。形式方法能做的貢獻是盡量提供更好的工具。在他退休並加入微軟劍橋研究中心後,他驚訝地發現 Hoare 邏輯斷言並不是用來證明程式正確性,而是用在測試並發現錯誤上。形式方法在除錯上的應用反倒比證明來得早。

Hoare 的邏輯斷言使用的是標準的邏輯與離散數學。我想後來許多程式語言學者的想法也是盡量設計符合數學模型的程式語言。Hoare 卻說近年來的發展剛好相反:許多數學概念為了分析程式語言的新功能(如物件、classes, heap, 指標等)而發展出來;大家開發新種類的代數,用來描述分散系統、並行系統等等。新的邏輯,如線性邏輯、分離邏輯等為了分析程式的行為而發明,有些還在其他的領域,如計算生物學、基因學、甚至社會學派上用場。

學者們一度相信要等到軟體錯誤造成了大災害,大家才會了解形式方法與軟體驗證的重要。事實卻不然。1996 年 Ariane V 火箭測試發射因軟體故障而失敗後,管理階層的策略是跑更多更嚴密的測試。越嚇他們,他們越會抱緊熟悉的方法不放。對軟體驗證的興趣反倒是從利潤出發:有效地使用形式方法會比較省錢。

而使軟體驗證流行的助力卻來自大家都沒想到的地方:駭客們。駭客攻擊造成大量的金錢損失,而駭客使用的軟體漏洞通常無法經由測試找到。唯一的可能是自動分析並驗證程式碼。這使得資訊安全成為軟體驗證的一大賣點,也由此漸漸推廣到汽車、電子產品、和航太產業中。

Hoare 接著談到業界與學界的不同使命。業界自然是使用最成熟的技術、解決最容易而迫切的問題。但學界的天職是完全相反的:建構最泛用的理論、解釋最多的現象、尋求可長可久的知識。不論哪種科學研究都嘗試回答這一系列的問題:這個東西做什麼?怎麼運作?為什麼能這麼運作?而有什麼證據顯示我們提出的答案是對的?在電腦科學中我們已經大致知道怎麼回答這些問題。一個程式的規格告訴我們它做什麼,斷言和其他內部模組、界面間的約定告訴我們他怎麼運作,程式語言語意解釋它為什麼能這麼運作,數學與邏輯證明增強我們的信心,而現在這些證明可以用電腦和工具產生和檢查。現在電腦科學家的舞台與使命是從事有說服力的實驗,檢驗這些工具和理論是否足以涵蓋今日大部分的程式、設計模式、語言、和應用。「實驗」在此的意義可能是現有應用程式的重新設計,從這些實驗得到的經驗將繼續推動理論與工具的進步。

Posted in 未分類 | 2 Comments

單子暖毛毛

既然談到了單子 (monad),重提一下去年在嵐達網貼的趣事

手工藝網站 Craft BitsWarm Fuzzy Friends.

Simon Peyton JonesPOPL 2003 受邀演講 Wearing the hair shirt: a retrospective on Haskell 中花了不少篇幅介紹單子,認為它是理論與實務的成功結合,並介紹了它的種種好處。Haskell 唯一的大錯誤,他說,是「單子」這冰冷生硬的數學名詞把人嚇跑了。我們應該把它取名為「暖毛毛(warm, fuzzy thing)」之類的。

此言一出,網路上真的出現了許多「暖毛毛」教學(例: eigenclass: Warm fuzzy things for random simulations)。剛好大約一年前,Henning Thielemann 決定釜底抽薪地讓網路上所有的 monad 都消失!例如,這是暖毛毛的 wiki page,裡頭有 Warm, fuzzy thing Transformers Explained, Warm, fuzzy thing/ST, 和 Research papers/Warm, fuzzy things and arrows 等等頁面。

Thielemann 事實上是寫了一個過濾器,把所有的 monad 字樣換成 warm, fuzzy thing, 單複數和詞性變化都考慮得不錯。連程式碼都溫暖了起來

class (Warm, fuzzy thing) a where
return :: b -> a b
(>>=) :: a b -> (b -> a c) -> a c
(>>) :: a b -> a c -> a c
fail :: String -> a b

-- instances:
instance (Warm, fuzzy thing) Maybe
instance (Warm, fuzzy thing) []
instance (Warm, fuzzy thing) IO

Warm, fuzzy thing> sequence $ words "Warm, fuzzy thing"
["M","o","n","a","d"]

且看這對推廣 Haskell 會不會有幫助吧!

Posted in 未分類 | Leave a comment

單子 (monad) 入門(一)

對於學函數語言的人來說,關於單子 (monad) 的種種似乎是最難跨越的門檻。許多朋友也常問哪有適合的入門教材,看來大家確實很需要一篇適合初學者讀的中文簡介。我試著以比較操作性的方式介紹單子,希望能有一些幫助。多年前我學函數編程時也對 monad 這東西覺得困惑不已,最後是讀了Philip Wadler 的這篇 The Essence of Functional Programming 才開始有「好像有點懂了」的感覺。該論文用一個直譯器當作貫穿全文的例子。我們也以類似的方式進行吧。

以下的資料結構表達一個只有整數、負號、和加法的數學式:

data Expr = Num Int | Neg Expr | Add Expr Expr

處理這種資料大概是函數語言的強項吧。例如,要算式子的值很容易:

eval :: Expr -> Int
eval (Num n) = n
eval (Neg e) = - (eval e)
eval (Add e1 e2) = eval e1 + eval e2

函數 eval 拿一個算式,傳回一個整數。看到 Num n 就直接傳回 n, 否則先把子算式的值算出,再取相反數或是求和。

假設我們添了一個整數除法運算元:

data Expr = Num Int | Neg Expr | Add Expr Expr | Div Expr Expr

我們便碰到了一個小難題。要怎麼處理分母是零的狀況呢?

Haskell 有一個 div 函數可做整數除法。碰到分母為零時,div 和大部分語言的除法函數一樣,丟出一個例外讓整個程式當掉。我們不希望這麼做,因此大概得在程式中先檢查一下看分母是否為零。但這時 eval 函數應該傳回什麼呢?


eval (Div e1 e2) = let v2 = eval e2
                   in if v2 == 0 then ??? else ...

用 Maybe 型別表達部份函數

有了除法後,eval 成了一個部份 (partial) 函數 — 某些輸入沒有對應的值。操作上,我們希望 Haskell 提供例外 (exception) 的功能,可以在程式另外某處將 eval 丟出的例外抓住。但例外是一種副作用。之前的函數編程簡介中提及,「函數語言沒有副作用」是個不精確的說法。函數語言程式終究也是得用到副作用的,只是我們會把用到的副作用納為數學模型的一部份,將他們的性質也描述出來。描述部份函數或例外的方法之一是用常見的 Maybe 型別:

data Maybe a = Just a | Nothing

eval 的型別改為 Expr -> Maybe Int. 正常運算結束便傳回 Just, 碰到分母為零的情形則傳回 Nothing. 呼叫 eval 的地方若得到 Nothing, 就相當於抓到了例外。

我們來看看這個版本的 eval. 碰到 Num n自然是傳回 Just n:

eval (Num n) = Just n

處理 Neg e 的條款則比以前稍微複雜了。我們得檢查 eval e 的結果,若是 Just v 便取 v 的相反數,但別忘了把結果也包上一個 Just. 如果遇到 Nothing, 表示 e 的運算失敗了,我們只好把 Nothing 再往上傳。

eval (Neg e) = case eval e of
                 Just v -> Just (-v)
                 Nothing -> Nothing

Add 的情況下,程式碼看來更冗長了些:

eval (Add e1 e2) = case eval e1 of
                    Just v1 ->case eval e2 of
                                Just v2 -> Just (v1 + v2)
                                Nothing -> Nothing
                    Nothing -> Nothing

我們得分別檢查 eval e1eval e2 的結果是 Just 或是 Nothing. 標成紅色的部份負責檢查例外的例行公事,是很機械性的程式碼。最後是 Div e1 e2 的情況,我們先計算 e2, 如果是零傳回 Nothing, 否則做除法運算。在這過程中我們也需要做許多分析檢查:

eval (Div e1 e2) = case eval e2 of
                    Just 0 -> Nothing
                    Just v2 -> case eval e1 of
                                Just v1 -> Just (v1 `div` v2)
                                Nothing -> Nothing
                    Nothing -> Nothing

很自然地,我們會希望把標成紅色的例行公事抽象掉。

Maybe 單子

我們再看一次處理 Neg 的條款:

eval (Neg e) = case eval e of
                 Just v -> Just (-v)
                 Nothing -> Nothing

我們真正想表達的僅是「把 eval e 的結果,如果有的話,送給 \v -> Just (-v)」。這只是多加了一點手續的函數應用 (application)。Haskell 有一個函數應用運算元,f $ x 就是把 x 餵給 f, 也就是 f x。也許我們可以自己定義一個函數應用運算元 =<<,把檢查 JustNothing 的動作藏在裡面:

eval (Neg e) = (\v -> Just (-v)) =<< eval e

習慣用函數 composition 的人可能會更想寫成 Just . negate =<< eval e,但目前的習慣是把這個運算元的左右顛倒:參數寫前面,函數寫後面。我們可以定義:

(>>=) : Maybe a -> (a -> Maybe b) -> Maybe b
(Just x) >>= f = f x
Nothing >>= f = Nothing

函數 eval 的前兩個條款便可以改寫如下:

eval (Num n) = return n
eval (Neg e) = eval e >>= (\v -> return (-v))

我們把 Just 寫成 return,等下會解釋為什麼。AddDiv 的情況也可以用 >>= 改寫:

eval (Add e1 e2) = eval e1 >>= \v1 ->
                   eval e2 >>= \v2 ->
                   return (v1 + v2)
eval (Div e1 e2) = eval e2 >>= \v2 ->
                   if v2 == 0 then mzero
                   else eval e1 >>= \v1 ->
                        return (v1 `div` v2)

處理 Add 的程式碼很清楚:先算出 eval e1, 把結果叫做 v1;再算 eval e2, 把結果叫做 v2, 然後相加。別忘了 v1 + v2 仍得用一個 return 轉成 Maybe 型別。遇到 Nothing 的狀況已在 >>= 的定義中處理掉了 -- eval e1 的結果若是 Nothing, 算式 eval e2 >>= ... 直接變成 Nothing 而不會算到 eval e2. 處理 Div 的程序也類似,如果 v2 為零,我們直接傳回 Nothing。此處把 Nothing 寫成 mzero, 含意待會兒解釋。

Maybe 是單子的一例。Haskell 中把單子定義成一個 type class:

class Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  return :: a -> m a

對任一個型別建構元 m, 如果我們能定義出 >>=return 兩個函數,並滿足後述的一些條件,m 就是一個單子。對 type class 我們不在此解釋太多,只需知道這是 Haskell 允許我們重載 (overload) >>=return 等符號、使許多型別的類似函數可以用同一組符號表示的機制就可以了。型別 m a 代表一個「結果為型別 a 的運算」,運算過程中可能產生單子 m 希望描述的副作用,如同 Maybe a 用來表示一個結果是 a, 但可能會產生例外的運算。函數 return 把一個型別為 a 的值「提升」到 m a. 在 Maybe 的例子中,return 就是 Just. 函數 >>= 則是提升到 m 之上的函數應用,左手邊是一個 m a,右手邊是一個從 am b 的函數;x >>= f 大致上的意思是執行 x 代表的運算,如果得到一個型別是 a 的值,把他傳給 f. 結果的型別是 m b. 我們等下會看到更多單子的例子。

上述的解釋是稍稍簡化過的版本。目前 Haskell 的 Monad class 中另有兩個 method, 在此省略不談。採用 return>>= 兩個 method 是 Haskell 為適合程式寫作選擇的設計。在更早的單子文獻中則用 return, map, join 三個運算元。這兩種定義是等價的。

單子定律

單子的 return>>= 兩個函數當然不能隨便寫。 型別建構元 m 要稱為單子,return>>= 須滿足下面三個定律:

  1. (return x) >>= f == f x,
  2. m >>= return == m,
  3. (m >>= f) >>= g == m >>= (\x -> f x >>= g).

頭兩條定律談到 return 的合理行為。第一條確保 return x 不含副作用: (return x) >>= f 應該和把 x 直接丟給 f 一樣。第二條定律中,把 m 的結果直接 return 回來並不改變其值。第三條是 >>= 的遞移律,可和函數組合的定義比較:

f (g x) = (f . g) x

這條定律確保 >>= 的行為確實類似函數應用。

讀者可以檢查一下 Maybereturn>>= 確實滿足這三條定律。目前 Haskell 本身無法自動檢查這三條定律,只能希望程式員遵守。程式員照理說也希望所有單子都滿足這些定律,以便於程式的推理分析。不幸的是確實有些很有用的「單子」為了效率因素會在某些情況下違反單子定律。以後有機會再談。

串列單子

我們進一步擴充算式,添加一個 Or 運算元:

data Expr = Num Int | Neg Expr | Add Expr Expr
          | Div Expr Expr | Or Expr Expr

此處的Or 倒不是邏輯上的「或」,而是非確定(non-deterministic)運算:Or e1 e2 的值可能是 e1, 也可能是 e2. 非確定運算元有點牽強地用在這裡僅是為了舉例,但在程式語言的應用中,需要處理非確定性的情形並不少見。例如一個文法 parse 一段句子,可能有不只一種 parse 的方法。我們會需要寫程式找出所有 parse.

我們希望找出一個算式所有可能的值,因此 eval 的型別改為 Expr -> [Int],將所有可能的值放在一個串列中。串列是另一個單子的常見例子。函數 return 將一個型別為 a 的值 x 提升成串列, 自然的選擇是傳回 [x], 因為 x 是自己的唯一值:

return :: a -> [a]
return x = [x]

假設 xs 是一個型別為 [a] 的串列,函數 f 拿一個 a, 將所有的可能結果放在型別為 [b] 的串列中。我們如何把 xs 餵給 f 呢?答案是先用 f 處理 xs 裡的每個元素,再把結果接起來:

(>>=) :: [a] -> (a -> [b]) -> [b]
xs >>= f = concat (map f xs)

寫成 list comprehension 可能更清楚: xs >>= f = [y | x <- xs, y <- f x]. 注意 return>>= 的型別分別是 a -> [a][a] -> (a -> [b]) -> [b], 符合 Monad class 的要求。(此處為了說明而標上型別。在 Haskell 中,由於型別已在 class 宣告中給過一次,在此是不加型別的。)

函數 eval 該怎麼處理新加的 Or 呢?Or e1 e2 的所有可能值是 e1 的所有可能值以及e2 的所有可能值,所以:

eval (Or e1 e2) = eval e1 ++ eval e2

而對於 Num, Neg, Add 等情況,很幸運地,eval 可在不修改的情況下直接使用新的 return>>= 定義。例如

eval (Add (Or (Num 1) (Num 3)) (Or (Num 3) (Num 4)))

的值會是 [4,5,6,7].

至於 Div 呢?函數 evalDiv 條款用了一個 mzero, 當時的值是 Nothing. 在此處只要把 mzero 設定為 [] 就可以了 -- 分母為零時 Div 沒有值,因此我們傳回空串列。

串列單子在此處用來表達非確定性計算,有時當我們說「非確定性單子」時,指的是串列。在 Haskell 這種緩式語言中,串列尾端在需要時才會算出來,因此 eval 的行為像是回溯 (backtracking):先用第一個值去試試看,如果可用就一直使用下去,如果失敗則回溯回來換成下一個值。讀者可以試試看 eval (Div (Num 4) (Add (Neg (Num 2)) (Or (Num 0) (Num 2)))) (4 / (-2 + (0 OR 2))) 是怎麼算出來的。有人也因此把串列稱作「回溯單子」。但不論非確定性或回溯還另有其他資料結構可表示(有的也許會特別強調公平性或效率等等因素)。此處我們還是簡單地稱之為串列單子。

MonadPlus

Maybe 與串列不僅是單子,他們都屬於單子的一個子類別。 如果在單子 m 上能定義出一個「加法」運算元和一個「零」,並滿足後述的一些條件,我們稱之為 MonadPlus:

class (Monad m) => MonadPlus m where
  mzero :: m a
  mplus :: m a -> m a -> m a

mzeromplus 至少應形成一個么半群(monoid)

  1. mzero `mplus` m = m,
  2. m `mplus` mzero = m,
  3. (m `mplus`n) `mplus` k = m `mplus` (n `mplus` k).

至於一些其他的條件則還沒有定論,可參照 Haskell Wiki 上的說明

操作上的直觀解釋是:mzero 代表一個沒有結果的空運算,mplus 則把兩個運算結果合併起來。串列的 mzeromplus 分別是 []++. MaybemzeroNothing, mplus 則可以定義為:

Nothing `mplus` m = m
(Just x) `mplus` m = Just x

也就是傳回第一個(最左邊的一個)結果。

模組化的功能代換

我們回顧一下最初的例子 --- 只有 Num, Neg, 和 Add 三個條款的 eval 函數:

eval :: Monad m => Expr -> m Int
eval (Num n) = return n
eval (Neg e) = eval e >>= (\v -> return (-v))
eval (Add e1 e2) = eval e1 >>= \v1 ->
                   eval e2 >>= \v2 ->
                   return (v1 + v2)

函數 eval 最一般的型別只要求 m 是某個單子。如果我們把 return 擦掉,把每個 m >>= f 代換為 f m,換句話說,把 return>>= 分別定義為:

return x = x
m >>= f = f m

稍微化簡一下,我們又得到了那個最簡單、沒有副作用的程式:

eval (Num n) = n
eval (Neg e) = - (eval e)
eval (Add e1 e2) = eval e1 + eval e2

這時 m a = a. 這也是一個單子,讀者可檢查滿足這個定義滿足單子三定律。我們稱之為「單位單子 (identity monad)」。1 單位單子是最基礎、不含副作用的單子。

我們可以把單子視為一種允許我們模組化地加入、抽換程式功能的方法。從上面的程式出發,如果我們為 eval 加上一個處理 Div 的條款, 由於其中用到了 mzero, Haskell 的型別系統會知道 m 必須是一個 MonadPlus:

eval :: MonadPlus m => Expr -> m Int

我們不能再選 m a = a 了。滿足 MonadPlus 要求的型別很多,Maybe 是其中的一個。

如果我們再加上一個 eval (Or ..) 條款(其中的 ++ 必須寫成 mplus),eval 最通用的型別仍不變。我們還是可以讓 m = Maybe,只是 Maybemplus 在碰到兩個 Just 時會選擇左邊的結果。而如果我們把 m a 選為 [a],同一個程式便會傳回所有結果形成的串列。

以後我們會看到更多這種例子:每個種類的單子提供一類副作用,如本文的例外、非確定性,或著環境、狀態 (state)、輸出入、續繼 (continuation)... Haskell 能由程式中使用的 method 判定我們需要哪一種單子,我們則可再選用符合條件的單子實際做出這些副作用。各種副作用可以這種模組化的方式加入程式中。

下次我們再看看其他常用的單子。

附註

  1. 可惜在 Haskell 中若要使用 type class, 我們必須定一個新的資料型別:data Id a = Id a。這麼一來 return>>= 的定義都會多一個資料建構元,看來不那麼清楚。此處先不談這點。

參考資料與延伸閱讀

  1. Philip Wadler. Monads for functional programming. In Marktoberdorf Summer School on Program Design Calculi, August 1992
  2. Ralf Hinze. Deriving backtracking monad transformers. ICFP 2000.
  3. Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry. Backtracking, interleaving, and terminating monad transformers. ICFP 2005.
Posted in 未分類 | 11 Comments