袁 曉 月

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

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

袁 曉 月

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

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

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

0 引言

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

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

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

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

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

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

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

3)射的復(fù)合。若A，B，C∈ob(A)，且有A(B，C)×A(A，B)→A(A，C)，簡(jiǎn)記為(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)，則存在一個(gè)稱為恒等射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)范疇中的對(duì)象具有ob(A)→ob(B)，記為A|→FA。

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

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

圖1 自然變換記號(hào)

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

定義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ù)式語(yǔ)言中的單子定義。為此，需要使用一些方法，以便函數(shù)語(yǔ)言中利用單子特性實(shí)現(xiàn)編程。通過(guò)引入Kleisli范疇可以實(shí)現(xiàn)范疇論中單子到函數(shù)式語(yǔ)言單子的轉(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范疇的另一種定義方式是引入運(yùn)算符(_)*，其中(_)*：A(A，TB)→A(TA，TB)，其表示將射f:A→T(B)中的A提升到計(jì)算T(A)，即f*:T(A)→T(B)。就是說(shuō)，f是從值到計(jì)算的函數(shù)，而f*是從計(jì)算到計(jì)算的函數(shù)。

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

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

2)范疇A中的對(duì)象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#語(yǔ)言的單子定義為Kleisli三元組，它有下列部件。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

identity{

let!a=getInt()

let!b=getInt()

return a+b}

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

let!pat=expr

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

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

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

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

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

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

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

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

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

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

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

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

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

3 結(jié)束語(yǔ)

基于文獻(xiàn)[5-6,10]的工作，本文給出從范疇單子(T,μ,η)到函數(shù)式語(yǔ)言F#單子(M,return,bind)轉(zhuǎn)換過(guò)程的數(shù)學(xué)解釋，討論了F#單子需要滿足的性質(zhì)。并給出了F#單子通用編程模板和常見的5種應(yīng)用情形。限于篇幅沒(méi)有給出樣例代碼和語(yǔ)法糖到常規(guī)代碼的對(duì)應(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ì)算機(jī)科學(xué)中的范疇論[M].合肥:中國(guó)科學(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-)，女，高級(jí)實(shí)驗(yàn)師，從事熱處理工作。

10.13990/j.issn1001-3679.2014.04.028

TP301.2

A

1001-3679(2014)04-0539-04