范疇單子在F#語言中的應(yīng)用研究

袁 曉 月

(江西省科學(xué)院應(yīng)用物理研究所，330029，南昌)

范疇單子在F#語言中的應(yīng)用研究

袁 曉 月

(江西省科學(xué)院應(yīng)用物理研究所，330029，南昌)

范疇論中的單子是包含一個函子和2個自然變換的三元組，而函數(shù)式F#語言中的單子則是由包含構(gòu)造子和return操作和bind操作的三元組。針對2種單子定義不一致的問題，首先給出了范疇單子的定義和性質(zhì)。在此基礎(chǔ)上，通過引入(_)*運算符，定義了Kleisli范疇。由此定義了函數(shù)語言F#單子。在此基礎(chǔ)上給出了F#單子滿足的性質(zhì)與范疇單子性質(zhì)的對應(yīng)關(guān)系。最后給出了F#單子常見的5種編程情形。

單子；范疇論；fsharp；函數(shù)式編程

0 引言

函數(shù)式語言的理論基礎(chǔ)是λ演算[1]。F#作為.NET框架上的靜態(tài)強(qiáng)類型通用函數(shù)式語言具有靜態(tài)類型推演特性[2-3]。這意味著F#可以編寫精簡、高效且錯誤少的代碼。單子是F#功能最為強(qiáng)大編程特性同時也是最難理解的部分。F#單子廣泛用于序列、異步計算和計算表達(dá)式編程中。對于輸入/輸出、變量賦值、異常處理、詞法分析、非確定性、并發(fā)和連續(xù)等具有副作用的函數(shù)式語言常規(guī)編程可以使用單子結(jié)構(gòu)描述。通過單子可以將這些具有副作用的功能編寫為純函數(shù)式語言，而無需擴(kuò)展函數(shù)式語言的語義。

F#語言單子編程對其構(gòu)造子中的return和bind操作函數(shù)特征及其滿足性質(zhì)給出了要求。但其與范疇單子定義及其性質(zhì)與對應(yīng)關(guān)系不夠嚴(yán)謹(jǐn)[4-6]。本文給出了完整的范疇單子到F#語言單子變換的數(shù)學(xué)描述，并給出了F#單子編程類型變換規(guī)則的數(shù)學(xué)解釋。在此基礎(chǔ)上給出了F#語言單子常用的5種應(yīng)用功能。

1 范疇單子與函數(shù)式語言范疇轉(zhuǎn)換

1.1范疇單子定義及其性質(zhì)

范疇論作為簡潔、統(tǒng)一的符號語言在代數(shù)學(xué)、邏輯學(xué)等許多數(shù)學(xué)分支和計算機(jī)的語義學(xué)、類型理論、程序驗證等方面有著廣泛的應(yīng)用。基于范疇論的觀點，函數(shù)式語言可以描述為由基元類型和類型變換函數(shù)構(gòu)成。通過函數(shù)復(fù)合機(jī)制可以生成更為復(fù)雜的類型與函數(shù)。基于文獻(xiàn)[4,7-9]工作給出單子定義。

定義1(范疇)：1)一個對象集合ob(A)，其元素稱為范疇A的對象。

2)一個射集A(A，B)或A→B。若A，B∈ob(A)，則存在從A到B的映射(簡稱為射或箭頭)，所有這些射構(gòu)成射集A(A，B)。

3)射的復(fù)合。若A，B，C∈ob(A)，且有A(B，C)×A(A，B)→A(A，C)，簡記為(g,f)|→g°f。稱g°f為從A到C的射，其由射g和射f復(fù)合。要求射復(fù)合滿足結(jié)合律，即：

(h°g)°f=h° (g°f)

其中：A，B，C，D∈ob(A)，f∈A(A，B)，g∈A(B，C)，h∈A(C，D)。

4)若A∈ob(A)，則存在一個稱為恒等射1A∈A(A，A)，其輸出恒等于輸入。

恒等射1A滿足單位律：

f°1A=f=1B°f

其中：A，B∈ob(A)，f∈A(A，B)。

定義2(函子)：若A，B是范疇，則函子F是從A到B的映射，其滿足：

1)范疇中的對象具有ob(A)→ob(B)，記為A|→FA。

3)對所有A∈A有F1A=1FA。

通常自然變換可以繪制成圖1所示的圖形。

圖1 自然變換記號

自然變換α:F→G可以理解為范疇A中的對象A經(jīng)過函子F對應(yīng)到范疇B的對象為FA。同樣，范疇A中的對象B經(jīng)過函子G對應(yīng)到范疇B的對象為GB。但范疇B中的對象GB可以由范疇B的對象FA經(jīng)過自然變換α得到。上述過程描述為：GB=α(FB)，記為G(B)=αF(B)。就是說，自然變換可以和函子復(fù)合。自然變換也可以稱為對象在范疇內(nèi)的滑動。

定義4(單子)：范疇A上的單子是三元組(T,μ,η)。其中T:A→A的函子。μ和η是滿足下列性質(zhì)的自然變換。

μ:T°T→T

η:1A→T

其滿足下列條件：

μ° (T°μ)=μ° (μ°T)。

μ°T°η=μ°η°T=1A。

自然變換μ和η可以用圖2所示表示。其中，自然變換μ具有乘積作用，自然變換η則具有單位變換作用。

圖2 自然變換μ和η的圖示

T,μ,η滿足圖3所示的結(jié)合律和單位律。

圖3 單子的性質(zhì)圖示

范疇論中的三元組(T,μ,η)單子定義僅僅解釋了單子需要滿足的性質(zhì)，并不能夠直接用于函數(shù)式語言中的單子定義。為此，需要使用一些方法，以便函數(shù)語言中利用單子特性實現(xiàn)編程。通過引入Kleisli范疇可以實現(xiàn)范疇論中單子到函數(shù)式語言單子的轉(zhuǎn)換[5,6,10]。

定義5(Kleisli范疇)：給定范疇A中單子(T,μ,η)，定義Kleisli范疇K如下：

ob(K)=ob(A)

K(A，B)=A(A，TB)

在范疇K，射的復(fù)合由下列公式求得：

g°Kf=μC°Tg°f

其中，f:A→T(B)，g:B→T(C)。

在范疇K的恒等射1A由下列公式給出：

1A=ηA

Kleisli范疇的另一種定義方式是引入運算符(_)*，其中(_)*：A(A，TB)→A(TA，TB)，其表示將射f:A→T(B)中的A提升到計算T(A)，即f*:T(A)→T(B)。就是說，f是從值到計算的函數(shù)，而f*是從計算到計算的函數(shù)。

范疇A中給定單子(T,μ,η)，其Kleisli范疇可以通過下列方法得到：

1)函子T:ob(A)→ob(A)。

2)范疇A中的對象A，定義ηA:A→T(A)。

3)范疇A中的射f:A→T(B)，定義f*:T(A)→T(B)。

其滿足下列性質(zhì)：

f*°ηA=f

(g*°f)*=g*°f*

其中，f:A→T(B)，g:B→T(C)。

1.2F#單子定義及其性質(zhì)

F#語言的單子定義為Kleisli三元組，它有下列部件。

1)類型構(gòu)造子M。對每個基礎(chǔ)類型，該構(gòu)造子定義了構(gòu)造對應(yīng)單子類型的方法。若M是單子名稱，t是基礎(chǔ)類型系統(tǒng)中的數(shù)據(jù)類型，則Mt是單子類型系統(tǒng)中對應(yīng)的類型。Mt同時是基礎(chǔ)類型系統(tǒng)中的一員。

2)return操作。return操作的函數(shù)特征為:t->Mt，其功能是將基礎(chǔ)類型中的值映射到對應(yīng)的單子類型中的值。

3)bind操作。其對應(yīng)的函數(shù)特征為：Mt*(t->Mu)->Mu。通過bind函數(shù)特征可以看到，bind操作能夠?qū)崿F(xiàn)單子類型間映射。后面將看到，bind操作是單子能夠按序執(zhí)行的關(guān)鍵。Bind操作的輸入部分函數(shù)特征為Mt*(t->Mu)表明F#中bind操作的2個參數(shù)必須是元組，這使得bind操作無法使用部分應(yīng)用。

F#單子操作滿足下列性質(zhì)：

1)右等同律，即bind(M,return)其結(jié)果為M。

2)左等同律，即bind((return x),f)等價于fx。

3)分配律，即bind(bind (m,f),g)等價于bind

(m,(fun x->bind(f x,g)))。

給定一個基礎(chǔ)類型系統(tǒng)，則單子是一種結(jié)構(gòu)，其嵌入相應(yīng)的類型系統(tǒng)中(該類型系統(tǒng)稱為單子類型系統(tǒng))到給定的基礎(chǔ)類型系統(tǒng)中。就是說，單子類型扮演基礎(chǔ)類型角色。

計算表達(dá)式的一般構(gòu)造過程為：

1)可選的定義一個類型，例如Identity。

2)定義構(gòu)造子類型IdentityBuilder，構(gòu)造子必須實現(xiàn)2個方法：return和bind。

3)實例化構(gòu)造子，其名稱為identity。

4)使用計算表達(dá)式完成計算。例如的代碼為：

identity{

let!a=getInt()

let!b=getInt()

return a+b}

計算表達(dá)式中由括號{ }包含的表達(dá)式常見語句包括：let!和do!。它們被稱為語法糖(Syntactic Sugar)。語法糖是指同樣一段代碼，可以使用不同的語法結(jié)構(gòu)實現(xiàn)。引入語法糖的目的是使得代碼簡明、可讀性好。工作流中大量使用語法糖來提高代碼的可讀性，例如，let!(和do!)是構(gòu)造類的bind方法的語法糖。對于計算表達(dá)式中的下列代碼：

let!pat=expr

cexpr//***后繼的計算表達(dá)式代碼

其實質(zhì)對應(yīng)的去糖化代碼為：

builder.bind(expr,(fun pat->cexpr))

由于bind的函數(shù)特征為：Mt*(t->Mu)->Mu，這要求let!pat=expr語句中的pat類型為t；expr的類型為Mt。bind操作是單子能夠?qū)崿F(xiàn)按序執(zhí)行的關(guān)鍵。

1.3F#單子的函數(shù)特征說明

對給定的函子T:A→B和范疇A中射f:A→B。則范疇A中的對象A在范疇B的對象為T(A)，且射T(f):T(A)→T(B)。在函數(shù)式語言中采用Kleisli范疇相似的三元組(M,return,bind)來定義單子。M表示函子T對象映射部分使用類型構(gòu)造子。例如，范疇A對象A的類型為t，則范疇B的對象T(A)的類型為Mt。return的功能與η相似，return操作的函數(shù)特征為:t->Mt。bind與Kleisli范疇的g*°f相同，bind操作對應(yīng)的函數(shù)特征為：Mt*(t->Mu)->Mu。

2 單子在F#語言中的應(yīng)用

函數(shù)式語言F#通過自定義單子bind操作的功能，用戶可以實現(xiàn)不同功能，這樣就有了實現(xiàn)不同目的的單子。使用單子實現(xiàn)的常見功能包括：

1)每步均返回成功或失敗的標(biāo)志，若成功則進(jìn)行下一步；任何一步失敗則退出整個計算。常見例子為FailureMonad或MaybeMonad。

2)由于單子的bind操作是自定義的，而不是語言特性，故可以完成下列自定義功能：忽略前2個異常，當(dāng)?shù)?個異常拋出時，退出整個計算。常見例子為ErrorMonad或ExceptionMonad，它被認(rèn)為是FailureMonad的擴(kuò)展。

3)計算表達(dá)式的每步返回一個多個結(jié)果集合，并使用bind操作對多個結(jié)果遍歷。使用這種方法，不需要在所有的地方編寫循環(huán)來處理多個結(jié)果，bind操作自動會處理多個。常見例子為ListMonad。

4)單子除了將一個結(jié)果從一步傳遞到下一步外，還可以使用bind操作傳遞額外的數(shù)據(jù)到下一步。該額外數(shù)據(jù)不會出現(xiàn)在源碼中，但你能夠依然從任何地方訪問該數(shù)據(jù)，而不需要手工將它傳遞到每個函數(shù)。常見例子為ReaderMonad。

5)使額外的數(shù)據(jù)可以被替換。這可以模仿破壞性更新，而實際上沒有執(zhí)行破壞性更新。常見例子為StateMonad或WriterMonad。

3 結(jié)束語

基于文獻(xiàn)[5-6,10]的工作，本文給出從范疇單子(T,μ,η)到函數(shù)式語言F#單子(M,return,bind)轉(zhuǎn)換過程的數(shù)學(xué)解釋，討論了F#單子需要滿足的性質(zhì)。并給出了F#單子通用編程模板和常見的5種應(yīng)用情形。限于篇幅沒有給出樣例代碼和語法糖到常規(guī)代碼的對應(yīng)關(guān)系表格。本文進(jìn)一步的研究包括單子在遞歸程序和圖形結(jié)構(gòu)中的應(yīng)用[4,11]。

[1]Barendregt H.Lambda Calculi with Types[M].Handbook of Logic in Computer Science,Volume Ⅱ,Abramsky S,Gabbay D M,Maibaum T S E,Clarendon Press,1992:117-309.

[2]Syme D,Granicz A,Cisternino A.Expert F# 3.0(3rd Edition)[M].New York:Apress,2013.

[3]Farmer W M.The seven virtues of simple type theory[J].Journal of Applied Logic,2007,11(001).

[4]G M P O,Gibbons J.Monads for behaviour[J].Electr Notes Theor Comput Sci,2013,298:309-324.

[5]Wadler P.Comprehending Monads[J].Mathematical structures in computer science,1992(2):461-493.

[6]Wadler P.Monads for Functional Programming[M].Advanced Functional Programming,Springer Verlag,LNCS 925,Meijer E,Springer Verlag,1995.

[7]Pierce B C.Basic Category Theory for Computer Scientists[M].Cambridge,Massachusetts:The MIT Press,1991.

[8]Barr M,Wells C.Category Theory for Computing Science (Second Edition)[M].Prentice-Hall International,1995.

[9]陳意云.計算機(jī)科學(xué)中的范疇論[M].合肥:中國科學(xué)技術(shù)大學(xué)出版社,1993.

[10]Erwig M,Ren D.Monadification of functional programs[J].Science of Computer Programming,2004,52(1/3):101-129.

[11]Kazana W,Segoufin L.Enumeration of monadic second-order queries on trees[J].ACM Trans Comput Log,2013,14(4):25.

ResearchontheApplicationofMonadofCategoryTheoryinFunctionalProgrammingF#

YUAN Xiaoyue

(Institute of Applicative Physics,Jiangxi Academy of Science,330029,Nanchang,PRC)

A monad of category theory is a triple,which has one functor and two natural transforms,as well as a monad of F# is also a triple,which has one constructor that includes two operator naming return function and bind function.The paper give a mathematical description to cover the gap between the two definitions.The Kleisli category was defined by the operator (_)*after the definition of category theory and its characters.Then the monad of F# and the correspondence of the characters between monad of category and F# was given.Finally,the five scenes of monad of F# were given.

monad;category theory;fsharp;functional programming

2014-06-13;

2014-07-14

袁曉月(1960-)，女，高級實驗師，從事熱處理工作。

10.13990/j.issn1001-3679.2014.04.028

TP301.2

A

1001-3679(2014)04-0539-04