強(qiáng)共歸納數(shù)據(jù)類型上的Comonadic共遞歸*

蘇錦鈿 余珊珊

(1.華南理工大學(xué) 計算機(jī)科學(xué)與工程學(xué)院，廣東 廣州 510006;2.廣東藥學(xué)院 醫(yī)藥信息工程學(xué)院，廣東 廣州 510006)

在范疇論的視角下，共歸納數(shù)據(jù)類型［1-2］可看成是某個共遞歸類型等式上的最大固定點(diǎn)，并且可抽象地描述為某個共代數(shù)函子的終結(jié)共代數(shù)［3-4］.由共歸納數(shù)據(jù)類型所對應(yīng)的終結(jié)共代數(shù)及其終結(jié)性可得到一種重要的共遞歸，稱為unfold［1-3］或atamorphism［4］，并可進(jìn)一步得到其他的共遞歸，如原始共遞歸或Course-of-Value 共遞歸［5］等.這些共遞歸操作滿足一系列的共代數(shù)計算律，在基于行為關(guān)系的函數(shù)定義和程序推理及轉(zhuǎn)換過程中具有重要的作用［6-7］.

筆者在前期工作中分別研究了共歸納數(shù)據(jù)類型上的共遞歸操作及其計算律，以及它們在計算機(jī)科學(xué)中的應(yīng)用［3，8］，并從雙代數(shù)的角度探討了歸納與共歸納數(shù)據(jù)類型、fold 與unfold 之間的關(guān)系［9］，但這些工作均沒有涉及到共歸納數(shù)據(jù)類型的強(qiáng)終結(jié)性及帶參數(shù)的共遞歸操作.作為范疇論編程語言Charity的基礎(chǔ)，強(qiáng)數(shù)據(jù)類型是指滿足一些額外性質(zhì)的數(shù)據(jù)類型［10］.目前對強(qiáng)數(shù)據(jù)類型的研究主要以強(qiáng)歸納數(shù)據(jù)類型［11-12］為主，即歸納數(shù)據(jù)類型所對應(yīng)的初始代數(shù)在參數(shù)下是初始的.Pardo［13-14］利用笛卡爾封閉范疇上的初始代數(shù)是強(qiáng)初始的性質(zhì)，給出了強(qiáng)歸納數(shù)據(jù)類型上的帶固定參數(shù)及累積參數(shù)的遞歸操作pfold 和afold 的定義，并結(jié)合積Comonad 對它們進(jìn)行結(jié)構(gòu)化描述.但Pardo 的研究主要針對強(qiáng)歸納數(shù)據(jù)類型及帶參數(shù)的遞歸操作，不適合直接應(yīng)用于共歸納數(shù)據(jù)類型.Cockett 等［15］雖然提出了強(qiáng)共歸納數(shù)據(jù)類型的概念，但沒有給出具體的證明，也沒有分析強(qiáng)共歸納數(shù)據(jù)類型上的各種計算律.

因此，在上述研究的基礎(chǔ)上，文中給出了強(qiáng)共歸納數(shù)據(jù)類型的定義及一種帶固定參數(shù)的共遞歸操作，稱為punfold;并結(jié)合Comonadic 共遞歸給出了unfold 和punfold 的一種統(tǒng)一的結(jié)構(gòu)化描述，同時分析了punfold 上的各種計算律.

1 相關(guān)理論

1.1 共代數(shù)和多項(xiàng)式函子

定義1 給定笛卡爾封閉范疇C 和C 上的自函子F:C →C，一個F-共代數(shù)定義為一個二元組(X，αX:X→FX)，其中X 稱為該F-共代數(shù)的載體，αX稱為該F-共代數(shù)的基調(diào).任意兩個F-共代數(shù)(X，αX:X→FX)和(Y，αY:Y→FY)間的同態(tài)射f:(X，αX)→(Y，αY)，是載體集上的射f:X →Y，且滿足等式αXf=FfαY.

若函子F 存在終結(jié)共代數(shù)，記為(νF，outF)，則對于任意一個F-共代數(shù)(X，αX)，總是存在從(X，αX)到(νF，outF)的唯一同態(tài)射unfoldF(αX):X→νF.unfoldF(αX)是由基調(diào)αX所確定的一個共遞歸，通常稱為unfold［1-3］或atamorphism［4］.

例1 參數(shù)化數(shù)組List［A］(記為A*，其中A 為某個已知的數(shù)據(jù)類型)可看成是函子L=1 +A ×X的終結(jié)共代數(shù)上的載體.數(shù)組A*上的基調(diào)包括一個謂詞操作isnil:X→1 +1(用于判斷數(shù)組是否為空)，以及兩個觀察操作head:X→A 和tail:X→X(用于給出數(shù)組的當(dāng)前元素及剩余部分).A*及其上的操作可表示為一個終結(jié)共代數(shù)結(jié)構(gòu):

(A*，outL=〈isnil，head，tail〉:A*→1 +A ×A*)，其中outL定義為(1 +〈head，tail〉)isnil?.

為了保證共代數(shù)函子存在相應(yīng)的終結(jié)共代數(shù)，只考慮以下的有限擴(kuò)展多項(xiàng)式函子［10］.

定義2 給定一個范疇C，稱自函子F:C→C 為有限擴(kuò)展多項(xiàng)式函子，當(dāng)且僅當(dāng)F 是由以下的函子類型歸納構(gòu)造而成:

其中:Id 為標(biāo)識函子;A 為A 上的常量函子;F+F 和F×F 分別為函子間的共積和積;F〈F，F(xiàn)，…，F(xiàn)〉(記為F〈Fi〉)為F:C→Cn與其他有限擴(kuò)展多項(xiàng)式函子F1，F(xiàn)2，…，F(xiàn)n的組合，可看成是映射為X →F(F1X，F(xiàn)2X，…，F(xiàn)nX)的函子，且F1，F(xiàn)2，…，F(xiàn)n均具有相同的元數(shù);Pow 為有限冪集函子;FA為指數(shù)函子，表示常量A 與函子F 間的一個函數(shù)關(guān)系.

根據(jù)文獻(xiàn)［16］中的定理10.6，上述函子均為有限的，因此存在著對應(yīng)的終結(jié)共代數(shù).例如，函子F(－)=1 +A×－的終結(jié)共代數(shù)為(A*，〈isnil，〈head，tail〉〉:A*→1 +A×A*)，給出了數(shù)組上所有可觀察行為的典型實(shí)現(xiàn).函子F(－)=A ×－的終結(jié)共代數(shù)為(A∞，〈value，next〉:A∞→A∞×X)，給出了所有無限流上的可觀察輸出值.

定義3 稱函子F:C→C 為強(qiáng)函子，當(dāng)且僅當(dāng)存在一個自然轉(zhuǎn)換:FX×Y→F(X ×Y)，滿足以下等式:

其中assX，Y，Z=〈〈fst，fstsnd〉，sndsnd〉:X ×(Y ×Z)→(X×Y)×Z 表示結(jié)合律的自然同構(gòu)射稱為函子F 的右強(qiáng)度，fst:X ×Y→X 和snd:X ×Y→Y分別為笛卡兒積上的左和右投影函數(shù).

對于笛卡爾封閉范疇來說，上述有限擴(kuò)展多項(xiàng)式函子都是強(qiáng)函子［17］，并且存在以下的射:

(1)自然同構(gòu)射dist:(X+Y)×Z→X×Z+Y×Z;

(2)applyA，X:XA×A→X，且對于任意一個射f:X×A→Y，都有一個唯一的射curry(f):X→YA與之對應(yīng)，使得f=applyA，Xcurry(f)×IdA.

對于指數(shù)函子FA，存在轉(zhuǎn)換:(FX)A→FXA，且可以歸納地定義如下:

其中G 為范疇C 上的有限擴(kuò)展多項(xiàng)函子，inl－1:X +Y→X 和inr－1:X +Y→Y 分別為左注入射(inl:X→X+Y)和右注入射(inr:Y→X+Y)的逆，表示共積到其左右分量的射.

1.2 Comonads

定義4 范疇C 上的Comonad 為一個三元組(D，ε，－D)，稱為coKleisli 三元組，其中為C 中對象間的函數(shù)關(guān)系，使得對于有εX:DX→X，對于f:DX→Y，有fD:DX→DY，且滿足以下等式:

(1)(εX)D=IdDX;

(2)對于射f:DX→Y，有fD;εY=f;

(3)對于任意兩個射f:DX→Y 和g:DY→Z，有fD;gD=(fD;g)D.

若將DX 看成是X 上的某種計算類型，D 為該計算的上下文環(huán)境，那么εX:DX→X 表示取出該計算環(huán)境中的值，fD:DX→DY 表示將f 擴(kuò)展為包含上下文環(huán)境的計算.例如，對于標(biāo)識Comonad D=Id，f:DX→Y 表示一般的確定性函數(shù)f:X→Y;對于積Comonad(或稱流Comonad［18］)D=Id ×A，f:DX→Y表示一個帶參數(shù)且類型為A 的確定性函數(shù)f:X ×A→Y，fD=〈f，snd〉:DX→DY 表示把計算源中的參數(shù)復(fù)制到輸出中.

定義5 給定范疇C 中的一個coKleisli 三元組(D，ε，–D)，對應(yīng)的coKleisli 范疇CD定義如下:

(1)CD中的對象與C 中的對象相同;

(2)CD中任意對象X 到Y(jié) 的射為C 中對應(yīng)的射f:DX→Y;

(3)CD中任意對象X 上的標(biāo)識射為εX:DX→X;

(4)CD中射f:DX→Y 與g:DY→Z 的組合為gfD:DX→Z.

為了區(qū)別于一般的射，將coKleisli 范疇中每一個形如f:DX→Y 的射稱為Comonadic 射.

定義6 給定范疇C 上的一個Comonad(D，ε，–D)和自函子F:C→C，則D 對F 的分配律為自然轉(zhuǎn)換:DFFD，且滿足以下等式:

(1)FεXX=εFX;

(2)F(IdDX)DX=DXDX(IdDFX)D.

對于函子F:C→C 及其上的Comonad(D，ε，－D)，若存在分配律:DFFD，則可定義函子:CD→CD，將對象X 映射為它自身F X=X，將Comonadic 射f:DX →Y 映射為F f=FfX:DFX→FY，將f:DX→Y和g:DY→Z 的組合gfD映射為(gfD)=(f )D:DX→FZ.F 可看成是函子F 在Comonad(D，ε，–D)及分配律:DFFD 下的一個函子化提升，稱為F 的Comonadic 提升或擴(kuò)展.

將形如(X，φX:DX→FX)的結(jié)構(gòu)稱為Comonadic F-共代數(shù)，記為FD-共代數(shù).任意兩個FD-共代數(shù)(X，φX:DX→FX)和(Y，φY:DY→FY)間的FD-共代數(shù)同態(tài)射f:(X，φX)→(Y，φY)為Comonadic 射f:DX→Y，且 滿 足YfD= F fφX.若 射f:X →Y 滿 足Df=FfφX，則稱f 為(X，φX)和(Y，φY)間的純FD-共代數(shù)同態(tài)射.

每個Comonad 下的所有FD-共代數(shù)及其同態(tài)射可構(gòu)成一個范疇，記為CDF.例如，對于標(biāo)識Comonad D=Id 和積Comonad D=Id ×A，CDF分別記為CIdF和若(νF，out'F:DνF→FνF)是范疇中的終結(jié)對象，那么總是存在從中任意一個對象(X，φX:DX →FX)到(νF，out'F)的唯一射unfoldF，D(φX):DX→νF，并且unfoldF，D(φX)為一個FD-共代數(shù)同態(tài)射.為了區(qū)別于一般的unfold，將形如coKleisli 范疇中的unfoldF，D(φX)射稱為Comonadic unfold.

2 強(qiáng)共歸納數(shù)據(jù)類型

給定范疇C 及其上的一個Comonad(D，ε，－D)，可定義一個從C 到CD的提升函子(－)#:C→CD，將范疇C 中的每一個對象X 映射為它本身(X)#=X，將C 中的每一個射f:X→Y 映射為f#=fεX:DX→Y，稱f#是f 在(D，ε，－D)下的一個Comonadic 提升.

命題1 對于任意的Comonad(D，ε，－D)，每一個F-共代數(shù)(X，αX:X→FX)滿足

證明 由(－)#和(－)D的定義可知命題1 成立.

證畢.

定義7 稱強(qiáng)函子F 的終結(jié)共代數(shù)(νF，outF)是強(qiáng)終結(jié)的，當(dāng)且僅當(dāng)對于對象A，提升fst:νF×A→FνF 是范疇中的一個終結(jié)對象.

命題2 笛卡爾封閉范疇上的終結(jié)共代數(shù)是強(qiáng)終結(jié)的.

證明 給定積Comonad D=Id ×A 及分配律 :DFFD，對于任意一個FD-共代數(shù)(X，φX:X ×A→FX)，可構(gòu)造射h=applyA，DX:(X ×A)A×A→F(X×A)和對應(yīng)的curry(h):(X ×A)A→(F(X ×A))A.再由可得到一個F-共代數(shù)curry(h):(X×A)A→F(X×A)A.

即圖1 中的左半部分滿足圖表交換條件.再由終結(jié)共代數(shù)的終結(jié)性可知(3)也滿足交換條件，其中f=unfoldF(k).因此，整個圖表滿足交換條件.知，對任意一個射f:(X ×A)A×A→νF，都存在另一

圖1 終結(jié)共代數(shù)的強(qiáng)終結(jié)性Fig.1 Strong finality of final coalgebras

由X×A 與(X ×A)A×A 間的一一對應(yīng)關(guān)系可個射f'= f〈curry(fst)，snd〉:X×A→νF 與之對應(yīng)，因此〈f，snd〉〈curry(fst)，snd〉=〈f〈curry(fst)，snd〉，snd〉=〈f'，snd〉.再由F f〈F curry(fst)，snd〉=F〈f〈curry(fst)，snd〉〉=F f'可知，f'是唯一射，且滿足:

因此，outF是強(qiáng)終結(jié)的，且有

證畢.

利用命題2 可以給出強(qiáng)歸納數(shù)據(jù)類型的定義.

定義8 稱一個共歸納數(shù)據(jù)類型是強(qiáng)共歸納類型，當(dāng)且僅當(dāng)該共歸納數(shù)據(jù)類型所對應(yīng)的終結(jié)共代數(shù)是強(qiáng)終結(jié)的.

由outF是同構(gòu)射的性質(zhì)，容易驗(yàn)證也是一個同構(gòu)射，因此可以作為范疇的一個終結(jié)FD-共代數(shù)，而任意一個FD-共代數(shù)(X，φX)到(νF)的唯一同態(tài)射f:DX→νF，實(shí)際上給出了一種帶固定參數(shù)的共遞歸計算，稱為punfold.

圖2 punfold 的定義Fig.2 Definition of punfold

每一個punfoldF(φX):X×A→νF 可以看成是:共遞歸的計算源包含了參數(shù)類型為A 的元素，并且該參數(shù)值在計算過程中保持不變.容易驗(yàn)證存在等式

圖3 punfold 的Comonadic 表示Fig.3 Comonadic expressions of punfold

命題3 每一個punfold 等價于積Comonad D=Id×A 下的Comonadic unfold 射.

證明 由定義9 及積Comonad 的定義可得

證畢.

例2 函數(shù)lmult:Nat*×Nat→Nat*將自然數(shù)數(shù)組Nat*中的每一個元素都分別乘以某個給定的自然數(shù)，即對于a，xNat 和xsNat*，lmult 定義為

lmult(［］，a)=［］，

lmult(x:xs，a)=(x×a):lmult(xs，a).

顯然，lmult 可定義為一個punfold:

lmult=punfoldL(mlist):Nat*×Nat→Nat*.

或者定義為積Comonad D=Id×Nat 下的Comonadic unfold:

unfoldF，Id×Nat(mlist):Nat*×Nat→Nat*.

其中基調(diào)mlist=〈m_isnil，m_head，m_tail〉:Nat*×Nat→1 +Nat ×Nat*中的操作m_isnil:Nat*×Nat→1 + 1、m_head:Nat*×Nat →Nat 和m_tail:Nat*×Nat→Nat*分別定義為

命題4 每一個unfold 都可以看成是計算過程中不使用參數(shù)的punfold，或者是任意范疇中的一個純FD-共代數(shù)同態(tài)射.

證明 由定義9 可知，每一個unfoldF(αX):X→νF 實(shí)際上相當(dāng)于在計算過程中不使用參數(shù)A 的punfold，并且在積Comonad D=Id ×A 下的Comonadic提升滿足(unfoldF(αX))#=punfoldF().顯然，對任意Comonads 下的范疇，unfoldF(αX)都是從(X)到(νF，)的一個純FD-共代數(shù)同態(tài)射.

證畢.

3 punfold 上的計算律

定律1(標(biāo)識律) 給定積Comonad D=Id ×A和分配律 :DFFD，強(qiáng)函子F 上的終結(jié)共代數(shù)(νF，outF)滿足punfoldF()=ενF.

證明 由積Comonad 下的Comonadic 提升和定義9 可知，F(xiàn)ενF()D=(ενF)D，即ενF為一個punfold，再由其唯一性知punfoldF)=ενF.

證畢.

定律2(消去律) 給定積Comonad D=Id ×A和分配律:DFFD，punfold 滿足:

證明 由定義9 和命題3 可得

證畢.

定律3(FD-共代數(shù)同態(tài)射融合律) 給定積Comonad D= Id×A 和分配律 :DFFD，一個punfold與一個FD-共代數(shù)同態(tài)射的組合仍是一個punfold，即

證明 由前提可知，圖4 中的(1)和(2)滿足圖表交換條件.因此，整個圖表也滿足交換條件.

證畢.

定律3 表示范疇CFId×A中的Comonadic unfold與一個Comonadic 射間的coKleisli 組合仍是一個Comonadic unfold.

圖4 punfold 與FD-共代數(shù)同態(tài)射間的組合定律Fig.4 Fusion law for punfold and FD-coalgebraic homomorphism

定律4(純FD-共代數(shù)同態(tài)射融合律) 給定積Comonad D= Id×A 和分配律 :DFFD，一個punfold與一個純FD-共代數(shù)同態(tài)射的組合仍是一個punfold:

證畢.

定律4 表明，在范疇CId×AF中的Comonadic unfold與一個純FD-共代數(shù)同態(tài)射的組合仍是一個Comonadic unfold.

例3 函數(shù)odd:Nat*→Nat*是積Comonad D=Id×Nat 下從(Nat*，olist=〈o_isnil，o_head，o_tail〉)到(Nat*，mlist=〈m_isnil，m_head，m_tail〉)的純FD-共代數(shù)同態(tài)射，用于取出Nat*中奇數(shù)位上的元素.基調(diào)olist=(1 +〈o_head，o_tail〉)o_isnil?中的操作分別定義為

o_isnil(xs，a)=isnil(xs)，

o_head(xs，a)=head(xs)×a，

o_tail(xs，a)=tail(tail(xs)).

根據(jù)定律4 可將函數(shù)odd 與例子2 中的函數(shù)lmult 合并為一個新的punfold，即

定律5(punfold 融合律) 給定積Comonad D=Id×A 和分配律:DFFD，若存在一個自然轉(zhuǎn)換子T:(DX →FX)→(DX →GX)，將 每 個FD-共 代 數(shù)(X，φX)映射為一個GD-共代數(shù)(X，T(φX))，將每個FD-共代數(shù)同態(tài)射f:(X，φX)→(Y，φY)映射為對應(yīng)的GD-共代數(shù)同態(tài)射，則兩個punfold punfoldF(φX)與punfoldG(T(out#F))之間的組合仍是一個punfold:punfoldG(T))punfoldF(φX)=punfoldG(T(φX)).

證明 令g=punfoldF(φX)，f=punfoldG(T)).

由前提及自然轉(zhuǎn)換子保持同態(tài)射的性質(zhì)可知，圖5中的(1)和(2)均滿足交換條件，且有G g(G f)D=G (gfD).再由終結(jié)共代數(shù)的強(qiáng)終結(jié)性及唯一性可知，gfD為一個punfold，即

證畢.

圖5 punfold 間的融合律Fig.5 Fusion law for punfold

定律6(punfold-unfold 融合律) 若存在一個自然轉(zhuǎn)換子S:(X→FX)→(DX→GX)，將每個F-共代數(shù)(X，αX:X→FX)映射為積Comonad D=Id ×A 下的GD-共代數(shù)(X，S(αX):DX→GX)，將每個F-共代數(shù)同態(tài)射f:(X，αX)→(Y，αY)映射為對應(yīng)的純GD-共代數(shù)同態(tài)射，則一個punfold f=punfoldF(φX)與一個unfold g=unfoldF(αX)的組合仍是一個punfold，即

punfoldG(S(outF))unfoldF(αX)×IdA=punfoldG(S(αX)).

證明 由前提和定律4 可容易得到

punfoldG(S(outF))unfoldF(αX)×IdA=punfoldG(S(αX)).

證畢.

利用上述各種融合律可以消去punfold 在計算過程中所產(chǎn)生的中間數(shù)據(jù)，從而簡化程序結(jié)構(gòu).

4 結(jié)語

目前，強(qiáng)歸納數(shù)據(jù)類型已經(jīng)成為一些函數(shù)式程序語言(如Charity)的基礎(chǔ).而強(qiáng)共歸納數(shù)據(jù)類型使得定義在共歸納數(shù)據(jù)類型上的共遞歸計算具備管理和操縱參數(shù)的能力，因此可以在計算源中包含額外的參數(shù)用于作為共遞歸計算的輸入，這不僅有助于提高共遞歸對動態(tài)行為的描述能力，可利用Comonads 與Monads 間的對偶性，將coKleisli 范疇對上下文依賴計算的結(jié)構(gòu)化描述與Kleisli 范疇對副作用計算的結(jié)構(gòu)化描述有機(jī)地融合起來，而且有助于促進(jìn)強(qiáng)共歸納數(shù)據(jù)類型和Comonads 在各種數(shù)據(jù)流編程語言(如Lucid、Lustre 或Lucide Synchrone等)、并行計算及其他更復(fù)雜的計算內(nèi)涵語義和上下文依賴計算研究中的應(yīng)用.

今后將繼續(xù)研究如何利用雙代數(shù)將強(qiáng)歸納數(shù)據(jù)類型和強(qiáng)共歸納數(shù)據(jù)類型統(tǒng)一起來，給出強(qiáng)抽象數(shù)據(jù)類型的定義及帶固定參數(shù)和累積參數(shù)的遞歸及共遞歸，并探討相應(yīng)的計算律.

［1］Hutton G.Fold and unfold for program semantics［C］∥Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming.New York:ACM，1998:280-288.

［2］Gibbons J，Jones G.The under-appreciated unfold［C］∥Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming.New York:ACM，1998:273-279.

［3］蘇錦鈿，余珊珊.共歸納數(shù)據(jù)類型上的共遞歸操作及其計算定律［J］.華南理工大學(xué)學(xué)報:自然科學(xué)版，2011，38(10):90-95.Su Jin-dian，Yu Shan-shan.Corecursion operations and its calculation laws on coinductive data types［J］.Journal of South China University of Technology:Natural Science Edition，2011，38(10):90-95.

［4］Meijer E，F(xiàn)okkinga M，Paterson R.Functional programming with bananas，lenses，envelopes and barbed wire［M］∥Functional Programming Languages and Computer Architecture.Berlin:Springer-Verlag，1991:215-240.

［5］Uustalu T，Vene V.Primitive (co)recursion and courseof-value (co)iteration，categorically［J］.Informatica，1999，10(1):5-26.

［6］Hinze R.Reasoning about codata ［C］∥Proceedings of the Third Summer School Conference on Central European Functional Programming School.Berlin:Springer-Verlag，2010:42-93.

［7］Vene V，Uustalu T.Functional programming with apomorphism(corecursion)［J］.Proceedings of the Estonian Academy of Science:Physics，Mathematics，1998，47(3):147-161.

［8］蘇錦鈿，余珊珊.程序語言中的共歸納數(shù)據(jù)類型及其應(yīng)用［J］.計算機(jī)科學(xué)，2011，38(11):114-118.Su Jin-dian，Yu Shan-shan.Coinductive data types and their applications in programming languages［J］.Computer Science，2011，38(11):114-118.

［9］蘇錦鈿，余珊珊.抽象數(shù)據(jù)類型的雙代數(shù)結(jié)構(gòu)［J］.華南理工大學(xué)學(xué)報:自然科學(xué)版，2011，39(12):1-7.Su Jin-dian，Yu Shan-shan.Bialgebraic structure of abstract data types［J］.Journal of South China University of Technology:Natural Science Edition，2011，39(12):1-7.

［10］Pardo A.A calculational approach to strong datatypes［R］.Norway:Department of Informatics，University of Oslo，1996.

［11］Greiner J.Programming with inductive and co-inductive types［R］.Pittsburgh:School of Computer Science，Carnegie-Mellon University，1992.

［12］Geuvers H.Inductive and coinductive types with iteration and recursion ［C］∥Proceedings of the Workshop on Types for Proofs and Programs.Bastad:Chalmers University，1992:193-217.

［13］Pardo A.Towards merging recursion and Comonads［C］∥Proceedings of the 2nd Workshop on Generic Programming.Utrecht:University of Utrecht，2000:50-68.

［14］Pardo A.Generic accumulations［C］∥Proceedings of IFIP TC2/WG2.1 Working Conference on Generic Programming.New York:ACM，2003:49-78.

［15］Cockett J R B，Spencer D.Strong categorical datatypes I［C］∥Proceedings of International Summer Category Theory Meeting 1991.Montreal:American Mathematical Society，1991:141-169.

［16］Rutten J J M M.Universal coalgebra:a theory of systems［J］.Theoretical Computer Science，2000，249(1):3-80.

［17］Kock A.Strong functors and monoidal Monads ［J］.Archiv der Mathematik，1972，23(1):113-120.

［18］Uustalu T，Vene V.Signals and Comonads［J］.Journal of Universal Computer Science，2005，22(7):1310-1326.