范畴单子在F#语言中的应用研究

袁 晓 月

(江西省科学院应用物理研究所，330029，南昌)

范畴单子在F#语言中的应用研究

袁 晓 月

(江西省科学院应用物理研究所，330029，南昌)

范畴论中的单子是包含一个函子和2个自然变换的三元组，而函数式F#语言中的单子则是由包含构造子和return操作和bind操作的三元组。针对2种单子定义不一致的问题，首先给出了范畴单子的定义和性质。在此基础上，通过引入(_)*运算符，定义了Kleisli范畴。由此定义了函数语言F#单子。在此基础上给出了F#单子满足的性质与范畴单子性质的对应关系。最后给出了F#单子常见的5种编程情形。

单子；范畴论；fsharp；函数式编程

0 引言

函数式语言的理论基础是λ演算[1]。F#作为.NET框架上的静态强类型通用函数式语言具有静态类型推演特性[2-3]。这意味着F#可以编写精简、高效且错误少的代码。单子是F#功能最为强大编程特性同时也是最难理解的部分。F#单子广泛用于序列、异步计算和计算表达式编程中。对于输入/输出、变量赋值、异常处理、词法分析、非确定性、并发和连续等具有副作用的函数式语言常规编程可以使用单子结构描述。通过单子可以将这些具有副作用的功能编写为纯函数式语言，而无需扩展函数式语言的语义。

F#语言单子编程对其构造子中的return和bind操作函数特征及其满足性质给出了要求。但其与范畴单子定义及其性质与对应关系不够严谨[4-6]。本文给出了完整的范畴单子到F#语言单子变换的数学描述，并给出了F#单子编程类型变换规则的数学解释。在此基础上给出了F#语言单子常用的5种应用功能。

1 范畴单子与函数式语言范畴转换

1.1范畴单子定义及其性质

范畴论作为简洁、统一的符号语言在代数学、逻辑学等许多数学分支和计算机的语义学、类型理论、程序验证等方面有着广泛的应用。基于范畴论的观点，函数式语言可以描述为由基元类型和类型变换函数构成。通过函数复合机制可以生成更为复杂的类型与函数。基于文献[4,7-9]工作给出单子定义。

定义1(范畴)：1)一个对象集合ob(A)，其元素称为范畴A的对象。

2)一个射集A(A，B)或A→B。若A，B∈ob(A)，则存在从A到B的映射(简称为射或箭头)，所有这些射构成射集A(A，B)。

3)射的复合。若A，B，C∈ob(A)，且有A(B，C)×A(A，B)→A(A，C)，简记为(g,f)|→g∘f。称g∘f为从A到C的射，其由射g和射f复合。要求射复合满足结合律，即：

(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经过函子F对应到范畴B的对象为FA。同样，范畴A中的对象B经过函子G对应到范畴B的对象为GB。但范畴B中的对象GB可以由范畴B的对象FA经过自然变换α得到。上述过程描述为：GB=α(FB)，记为G(B)=αF(B)。就是说，自然变换可以和函子复合。自然变换也可以称为对象在范畴内的滑动。

定义4(单子)：范畴A上的单子是三元组(T,μ,η)。其中T:A→A的函子。μ和η是满足下列性质的自然变换。

μ:T∘T→T

η:1A→T

其满足下列条件：

μ∘ (T∘μ)=μ∘ (μ∘T)。

μ∘T∘η=μ∘η∘T=1A。

自然变换μ和η可以用图2所示表示。其中，自然变换μ具有乘积作用，自然变换η则具有单位变换作用。

图2 自然变换μ和η的图示

T,μ,η满足图3所示的结合律和单位律。

图3 单子的性质图示

范畴论中的三元组(T,μ,η)单子定义仅仅解释了单子需要满足的性质，并不能够直接用于函数式语言中的单子定义。为此，需要使用一些方法，以便函数语言中利用单子特性实现编程。通过引入Kleisli范畴可以实现范畴论中单子到函数式语言单子的转换[5,6,10]。

定义5(Kleisli范畴)：给定范畴A中单子(T,μ,η)，定义Kleisli范畴K如下：

ob(K)=ob(A)

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

在范畴K，射的复合由下列公式求得：

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是从值到计算的函数，而f*是从计算到计算的函数。

范畴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)。

其满足下列性质：

f*∘ηA=f

(g*∘f)*=g*∘f*

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

1.2F#单子定义及其性质

F#语言的单子定义为Kleisli三元组，它有下列部件。

1)类型构造子M。对每个基础类型，该构造子定义了构造对应单子类型的方法。若M是单子名称，t是基础类型系统中的数据类型，则Mt是单子类型系统中对应的类型。Mt同时是基础类型系统中的一员。

2)return操作。return操作的函数特征为:t->Mt，其功能是将基础类型中的值映射到对应的单子类型中的值。

3)bind操作。其对应的函数特征为：Mt*(t->Mu)->Mu。通过bind函数特征可以看到，bind操作能够实现单子类型间映射。后面将看到，bind操作是单子能够按序执行的关键。Bind操作的输入部分函数特征为Mt*(t->Mu)表明F#中bind操作的2个参数必须是元组，这使得bind操作无法使用部分应用。

F#单子操作满足下列性质：

1)右等同律，即bind(M,return)其结果为M。

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

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

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

给定一个基础类型系统，则单子是一种结构，其嵌入相应的类型系统中(该类型系统称为单子类型系统)到给定的基础类型系统中。就是说，单子类型扮演基础类型角色。

计算表达式的一般构造过程为：

1)可选的定义一个类型，例如Identity。

2)定义构造子类型IdentityBuilder，构造子必须实现2个方法：return和bind。

3)实例化构造子，其名称为identity。

4)使用计算表达式完成计算。例如的代码为：

identity{

let!a=getInt()

let!b=getInt()

return a+b}

计算表达式中由括号{ }包含的表达式常见语句包括：let!和do!。它们被称为语法糖(Syntactic Sugar)。语法糖是指同样一段代码，可以使用不同的语法结构实现。引入语法糖的目的是使得代码简明、可读性好。工作流中大量使用语法糖来提高代码的可读性，例如，let!(和do!)是构造类的bind方法的语法糖。对于计算表达式中的下列代码：

let!pat=expr

cexpr//***后继的计算表达式代码

其实质对应的去糖化代码为：

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

由于bind的函数特征为：Mt*(t->Mu)->Mu，这要求let!pat=expr语句中的pat类型为t；expr的类型为Mt。bind操作是单子能够实现按序执行的关键。

1.3F#单子的函数特征说明

对给定的函子T:A→B和范畴A中射f:A→B。则范畴A中的对象A在范畴B的对象为T(A)，且射T(f):T(A)→T(B)。在函数式语言中采用Kleisli范畴相似的三元组(M,return,bind)来定义单子。M表示函子T对象映射部分使用类型构造子。例如，范畴A对象A的类型为t，则范畴B的对象T(A)的类型为Mt。return的功能与η相似，return操作的函数特征为:t->Mt。bind与Kleisli范畴的g*∘f相同，bind操作对应的函数特征为：Mt*(t->Mu)->Mu。

2 单子在F#语言中的应用

函数式语言F#通过自定义单子bind操作的功能，用户可以实现不同功能，这样就有了实现不同目的的单子。使用单子实现的常见功能包括：

1)每步均返回成功或失败的标志，若成功则进行下一步；任何一步失败则退出整个计算。常见例子为FailureMonad或MaybeMonad。

2)由于单子的bind操作是自定义的，而不是语言特性，故可以完成下列自定义功能：忽略前2个异常，当第3个异常抛出时，退出整个计算。常见例子为ErrorMonad或ExceptionMonad，它被认为是FailureMonad的扩展。

3)计算表达式的每步返回一个多个结果集合，并使用bind操作对多个结果遍历。使用这种方法，不需要在所有的地方编写循环来处理多个结果，bind操作自动会处理多个。常见例子为ListMonad。

4)单子除了将一个结果从一步传递到下一步外，还可以使用bind操作传递额外的数据到下一步。该额外数据不会出现在源码中，但你能够依然从任何地方访问该数据，而不需要手工将它传递到每个函数。常见例子为ReaderMonad。

5)使额外的数据可以被替换。这可以模仿破坏性更新，而实际上没有执行破坏性更新。常见例子为StateMonad或WriterMonad。

3 结束语

基于文献[5-6,10]的工作，本文给出从范畴单子(T,μ,η)到函数式语言F#单子(M,return,bind)转换过程的数学解释，讨论了F#单子需要满足的性质。并给出了F#单子通用编程模板和常见的5种应用情形。限于篇幅没有给出样例代码和语法糖到常规代码的对应关系表格。本文进一步的研究包括单子在递归程序和图形结构中的应用[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]陈意云.计算机科学中的范畴论[M].合肥:中国科学技术大学出版社,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