计算机科学 ›› 2016, Vol. 43 ›› Issue (10): 9-18.doi: 10.11896/j.issn.1002-137X.2016.10.002

• 目次 • 上一篇    下一篇

计算机科学中的范畴数据类型的研究综述

苏锦钿   

  1. 华南理工大学计算机科学与工程学院 广州510640
  • 出版日期:2018-12-01 发布日期:2018-12-01
  • 基金资助:
    本文受广东省自然科学基金(2015A030310318),广东省医学科学技术研究基金项目(A2015065),国家自然科学基金资助

Survey on Categorical Data Type in Computer Science

SU Jin-dian   

  • Online:2018-12-01 Published:2018-12-01

摘要: 范畴数据类型是指以范畴论为数学理论基础研究数据类型的描述、计算、语义和应用。早期的范畴数据类型研究以归纳数据类型为主,采用代数从归纳的角度研究有限数据类型的构造语义和递归性质。近年来,归纳数据类型的对偶概念——共归纳数据类型逐渐引起计算机科学工作者的关注与研究,他们采用共代数从观察的角度研究无限数据类型的行为语义和共递归性质。利用范畴论可以为数据类型研究提供统一的数学理论基础,并将代数和共代数中的各种重要研究成果有机地融合在一起,如语法构造与动态行为、递归与共递归、同余与互模拟等。目前,范畴数据类型已经在程序语言、计算描述、理论证明器和并行计算等领域得到广泛的应用。对范畴数据类型的基本概念、数学理论基础、逻辑基础及应用等方面的最新研究成果进行介绍,以引起国内外相关研究领域的学者对计算机科学中的范畴数据类型理论的关注。

关键词: 数据类型,范畴论,代数,共代数,逻辑演算,程序语言

Abstract: Categorical data type refers to using category theory as the mathematical foundations for the researches on the description,computation,semantic and application of data types.The earlier work focuses on inductive data type and uses algebras to describe the construction semantics and recursive properties of finite data type from the inductive perspective.In recent years,coinductive data type,the dual concept of inductive data type,has attracted the attentions of many computer scientists,which use coalgebras to describe the behavioral semantics and corecursive properties of infinite data type from the observational perspective.Category theory can offer a unified mathematical theory foundation for various data types to discuss many important relations and properties,and integrate various important achievements of algebras and coalgebras,i.e.syntactic constructions and dynamic behaviors,recursion and corecursion,congruence and bisimulation and so on.Currently,categorical data type has been widely applied in many fields,such as programming languages,descriptions of calculation,theorem provers and parallel computations,etc.The latest research results of categorical data type in its basic concepts,mathematical foundations,logical foundations and their applications were introducted to attract the attention of the relative researchers.

Key words: Data type,Category theory,Algebra,Coalgebra,Logical calculus,Programming language

[1] 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 (in Chinese) 苏锦钿,余珊珊.共归纳数据类型上的共递归操作及其计算定律[J].华南理工大学学报(自然科学版),2011,38(10):90-95
[2] Su Jin-dian,Yu Shan-shan.Coinductive Data Types and theirApplications in Programming Languages[J].Computer Science,2011,38(11):114-118 (in Chinese) 苏锦钿,余珊珊.程序语言中的共归纳数据类型及其应用[J].计算机科学,2011,38(11):114-118
[3] Hinze R.Reasoning about Codata [M]∥ LNCS 6299.Berlin: Springer-Verlag,2010:42-93
[4] Hagino T.A Categorical Programming Language[D].University of Edinburgh,1987:8-56
[5] Hagino T.Codatatypes in ML[J].Journal of Symbolic Computation,1989,8(6):629-650
[6] Wralth G C.A Note on Categorical Datatypes[M]∥LNCS 389.Berlin:Springer-Verlage,1989:118-127
[7] Malcolm G.Data Structures and Program Transformation[J].Science of Computer Programming,1990,14(2/3):255-279
[8] Meijer E,Fokkinga M,Paterson R.Functional Programmingwith Bananas,Lenses,Envelopes and Barbed Wire[M]∥Functional Programming Languages and Computer Architecture,LNCS 523.Berlin:Springer-Verlag,1991:215-240
[9] Geuvers H.Inductive and Coinductive Types with Iteration and Recursion[C]∥Informal Proceedings of the Workshop on Types for Proofs and Programs.Bastad,Sweden,1992:193-217
[10] Greiner J.Programming with Inductive and Co-inductive Types [R].Tech.Report CMU-CS-92-109,School of Computer Science,Pittsburgh:Carnegie-Mellon University,1992
[11] Cockett J R B,Spencer D.Strong Categorical Datatypes II:A Term Logic for Categorical Programming[J].Theoretical Computer Science,1995,139(1):69-113
[12] Skillicorn D B.Structuring Data Parallelism Using Categorical Data Types[C]∥Programming Models for Massively Parallel Computers.Berlin:Computer Society Press,1993:110-115
[13] Skillicorn D B.Parallel Implementation of Tree Skeletons[J].Journal of Parallel and Distributed Computing,1996,39(2):115-125
[14] Fokinga M M.Datatype Laws without Signatures[J].Mathematical Structures in Computer Science,1996,6(1):1-32
[15] Erwig M.Metamorphic Programming:Structured Recursion for Abstract Data Types[R].Technical Report 242,FernUniversit at Hagen,1998
[16] Vesely P M.Categorical Combinators for Charity[D].The University of Calgary,1997:48-63
[17] Pardo A.A Calculational Approach to Strong Datatypes[R].8th Nordic Workshop on Programming Theory.Research Report 240,Norway,University of Oslo,1997
[18] Pardo A.Towards Merging Recursion and Comonads[R].Technical Report UU-CS-2000-19,University of Utrecht,2000:50-68
[19] Uustalu T,Vene V.Primitive (Co) Recursion and Course-of-Value (Co)Iteration,Categorically[J].Informatica,1999,10(1):5-26
[20] Cunha M A.Recursion Patterns as Hylomorphisms [R].Technical report DI-PURe-03.11.01,Department of Informatics,University of Minho,2003
[21] Dominguez F,Pardo A.Program Fusion with Paramorphisms[C]∥Mathematically Structured Functional Programming(MSFP’06).British:British Computer Society,2006
[22] Uustalu T,Vene V.Mendler-style Inductive Types,Categorically[J].Nordic Journal of Computing,1999,6(3):343-361
[23] Vene V.Categorical Programming with Inductive and Coinductive Types[D].University of Tartu,2000:63-97
[24] Cirstea C.A Coalgebraic Equational Approach to Specifying Observational Structures[J].Theoretical Computer Science,2002,280(1/2):35-68
[25] Leivant D,Ramyaa R.Implicit Complexity for Coinductive Data:a Characterization of Corecurrence[J].Electronic Proceedings in Theoretical Computer Science,2012,75:1-14
[26] Bird R,Paterson R.Generalised Folds for Nested Datatypes[J].Formal Aspects of Computing,1999,11(2):200-222
[27] Hinze R.Polytypic Functions over Nested Datatypes[J].Dis-crete Mathematics and Theoretical Computer Science,1999,3(4):193-214
[28] Blampied P A.Structured Recursion for Non-uniform Data-Types[D].University of Nottingham,2000
[29] Abel A,Matthes R,Uustalu T.Generalized Iteration and Coitera-tion for Higher-Order Nested Datatypes[C]∥Foundations of Software Science and Computation Structures(FoSSaCS 2003).LNCS 2620,Berlin:Springer-Verlag,2003:54-69
[30] Traytel D,Popescu A,Blanchette J C.Foundational,Compositional (Co)datatypes for Higher-Order Logic:Theory Applied to Theorem Proving[C]∥Twenty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2012).2012:595-605
[31] Awodey S.Category Theory[M].Oxford University Press,2006:265-290
[32] Gibbons J,Hutton G,Altenkirch T.When is a Function a Fold or an Unfold?[J].Electronic Notes in Theoretical Computer Science,2001,44(1):146-160
[33] Guguen J,Rosu G.Hiding More of Hidden Algebra[C]∥World Congress on Formal Methods,LNCS 1709.Berlin:Springer-Verlag,1999:1704-1719
[34] Erwig M.Random Access to Abstract Data Types[C]∥Pro-ceedings of AMAST.2000:135-149
[35] Nogueira P,Moreno-Navarro J J.Bialgebra Views:A Way for Polytypic Programming to Cohabit with Data Abstraction[C]∥Proceedings of the ACM SIGPLAN Workshop on Generic Programming 2008.NY:ACM,2008:61-73
[36] Rutten J J M M.Universal Coalgebra:a Theory of Systems[J].Theoretical Computer Science,2000,249(1):3-80
[37] Erwig M.Categorical Programming with Abstract Data Types[M]∥7th Int.Conf.on Algebraic Methodology and Software Technology,LNCS 1548.Berlin:Springer-Verlag,1998:406-421
[38] Fokkinga M M,Meijer E.Program Calculation Properties ofContinuous Algebras[R].Technical Report CS-R9104,CWI,Amsterdam,1991
[39] Cockett J R,Santocanale L.Induction,Coinduction,and Adjoints[J].Electronic Notes in Theoretical Computer Science,2003,69(1):101-119
[40] Mycroft A.Polymorphic Types Schemes and Recursive Definitions [C]∥Proceedings of International Symposium on Programming.1984:217-228
[41] Chuang T R,Lin J L.An Algebra of Dependent Data Types[R].Technical Report TR-IIS-06-012,Institute of Information Science,Taiwan:Academia Sinica,2006
[42] Capretta V,Uustalu T,Vene V.Corecursive Algebras:a Study of General Corecursion[M]∥12th Brazilian Symp.on Formal Methods(SBMF 2009),LNCS 5902.Berlin:Springer-Verlag,2009:84-100
[43] Bonsangue M,Rot J,Ancona D,et al.A Coalgebraic Foundation for Coinductive Union Types[C]∥ICALP 2014,LNCS 8573.Berlin:Springer-Verlag,2014:62-73
[44] Su Jin-dian,Yu Shan-shan.Subtype of Categorical Data Types[J].Journal of South China University of Technology(Natural Science Edition),2013,41(9):58-64 (in Chinese) 苏锦钿,余珊珊.范畴数据类型上的子类型[J].华南理工大学学报(自然科学版),2013,41(9):58-64
[45] Miranda-Perea F E.Some Remarks on Type Systems forCourse-of-Value Recursion[J].Electronic Notes in Theoretical Computer Science,2009,247(1):103-121
[46] Jeannin J B,Kozen D,Silva A.Language Constructs for Non-well- Founded Computation[C]∥ESOP 2013,LNCS 7792.Berlin:Springer-Verlag,2013:61-80
[47] Hinze R,Wu N,Gibbons J.Conjugate Hylomorphisms[C]∥POPL’15.2015
[48] Clouston R,Bizjak A,Grathwohl H B,et al.Programming and Reasoning with Guarded Recursion for Coinductive Types[C]∥FoSSaCS 2015.2015
[49] Su Jin-dian,Yu Shan-shan.Generalised Coiteration and its Calculational Laws[J].Journal of South China University of Technology(Natural Science Edition),2012,40(9):62-68 (in Chinese) 苏锦钿,余珊珊.广义共迭代及其计算律[J].华南理工大学学报(自然科学版),2012,40(9):62-68
[50] Su Jin-dian,Yu Shan-shan.Corecursive Operations with Parameters and the Associated Calculational Laws[J].Journal of Computer Research and Development,2013,50(12):2672-2690 (in Chinese) 苏锦钿,余珊珊.带参数的共递归操作及其计算定律[J].计算机研究与发展,2013,50(12):2672-2690
[51] Yu Shan-shan,Li Shi-xian,Su Jin-dian.Hylomorphisms withParameters and its Associated Calculational Laws[J].Journal of Computer Research and Development,2013,50(3):602-618 (in Chinese) 余珊珊,李师贤,苏锦钿.一种带参数的Hylomorphisms及其计算律[J].计算机研究与发展,2012,50(3):502-618
[52] Abel A,Matthes R.(Co-)Iteration for Higher-Order NestedDatatypes[M]∥Types for Proofs and Programs,Internat.Workshop,TYPES 2002,LNCS 2646.Berlin:Springer-Verlag,2003:1-20
[53] Uustalu T,Vene V.The Recursion Scheme From the Cofree Recursive Comonad[J].Electric Notes in Theoretical Computer Science,2011,229(5):135-157
[54] Su Jin-dian,Yu Shan-shan.Comonadic Corecursions on StrongCoinductive Datatypes[J].Journal of South China University of Technology(Natural Science Edition),2014,42(1):128-134 (in Chinese) 苏锦钿,余珊珊.强共归纳数据类型上的Comonadic共递归[J].华南理工大学学报(自然科学版),2014,42(1):128-134
[55] Capretta V,Uustalu T,Vene V.Recursive Coalgebras fromComonads[J].Information and Computation,2006,204(4):437-468
[56] Pardo A.Monadic Corecursion-Definition,Fusion Laws,and Applications[C]∥Coalgebraic Methods in Computer Science,Electronic Notes in Theoretical Computer Science.1998,11:105-139
[57] Su Jin-dian,Yu Shan-shan.Monadic Recursions with Fixed Parameters[J].Journal of South China University of Technology(Natural Science Edition),2014,42(7):33-39,3 (in Chinese) 苏锦钿,余珊珊.带固定参数的Monadic递归[J].华南理工大学学报(自然科学版),2014,42(7):33-39,3
[58] Gianantonio P D,Miculan M.Unifying Recursive and Co-recursive Definitions in Sheaf Categories [C]∥FoSSaCS 2004,LNCS 2987.Berlin:Springer-Verlag,2004:136-150
[59] Hinze R.Adjoint Folds and Unfolds,or:Scything Through the Thicket of Morphisms[C]∥Proceedings of the 10th International Conference on Mathematics of Program Construction (MPC’10),LNCS 6120.Berlin:Springer-Verlag,2010:195-228
[60] Hinze R.Type Fusion[C]∥Proceedings of the Thirteenth Inter-national Conference on Algebraic Methodology and Software Technology,LNCS 6486.Berlin:Springer-Verlag,2010:92-110
[61] Fumex C,Ghani N,Johnn P.Indexed Induction and Coinduc-tion,Fibrationally[C]∥CALCO 2011,LNCS 6859.Berlin:Springer-Verlag,2011:176-191
[62] Glimming J.Parametric (Co)Iteration vs.Primitive Direcursion[C]∥CALCO 2007,LNCS 4624.Berlin:Springer-Verlag,2007:257-278
[63] 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):44-50,63 (in Chinese) 苏锦钿,余珊珊.抽象数据类型的双代数结构[J].华南理工大学学报(自然科学版),2011,39(12):44-50,63
[64] Su Jin-dian,Yu Shan-shan.Bialgebraic Structures of Abstract Data Types and its Calculational Laws[J].Journal of Computer Research and Development,2012,49(8):1787-1803 (in Chinese) 苏锦钿,余珊珊.抽象数据类型的双代数结构及其计算定律[J].计算机研究与发展,2012,49(8):1787-1803
[65] Bartels F.Generalised Coinduction[J].Electronic Notes in Theo-retical Computer Science,2001,44(1):67-87
[66] Cancila D,Honsell F,Lenisa M.Generailzed Coiteration Schemata [J].Electronic Notes in Theoretical Computer Science,2003,82(1):76-93
[67] Zhou Xiao-cong,Shu Zhong-mei.A Survey on the Coalgebraic Methods in Computer Science[J].Journal of Software,2003,14(10):1661-1671 (in Chinese) 周晓聪,舒忠梅.计算机科学中的共代数方法的研究综述[J].软件学报,2003,14(10):1661-1671
[68] Gumm H P.Universal Coalgebras and their Logics[J].AJSE- Mathematics,2009,1(1):105-130
[69] Schrder L.Coalgebraic Modal Logic in CoCASL[M]∥RecentTrends in Algebraic Development Techniques,LNCS 4409.Berlin:Springer-Verlag,2007:127-141
[70] Simon L.Extending Logic Programming with Coinduction[D].University of Texas at Dallas Richardson,2007
[71] Hasuo I,Cho K,Kataoka T,et al.Coinductive Predicates and Final Sequences in a Fibration[J].Electronic Notes in Theoretical Computer Science,2013,298(1):197-214
[72] Mossakowski T,Schrdera L,Roggenbachb M,et al.Algebraic- coalgebraic Specification in CoCASL[J].Journal of Logic and Algebraic Programming,2006,67(1/2):146-197
[73] Klin B.Bialgebraic Methods and Modal Logic in Structural Ope-rational Semantics[J].Information and Computation,2009,207(2):237-257
[74] Cockett J R B,Fukushima T.About Charity[R].Technical Report 92/480/18,Dep.Comp.Sci.,Univ.Calgary.1992
[75] Johnn P,Ghani N.Haskell Programming with Nested Types:A Principled Approach[J].Higher-Order and Symbolic Computation,2010,22(2):155-189
[76] Capretta V.Coalgebras in Functional Programming and TypeTheory[J].Theoretical Computer Science,2011,412(38):5006-5024
[77] Kurz A,Petrisan D,Severi P.Nominal Coalgebraic Data Types With Applications to Lambda Calculus[J].Logical Methods in Computer Science,2013,9(4):1-51
[78] Simon L,Mallya A,Bansal A,et al.Coinductive Logic Programming [M]∥Etalle S,Truszczynski M.eds.,ICLP 2006,LNCS4079.Berlin:Springer-Verlag,2006:330-344
[79] Simon L,Bansal A,Mallya A,et al.Co-Logic Programming:Extending Logic Programming with Coinduction[M]∥ICALP 2007,LNCS 4596.Berlin:Springer-Verlag,2007:472-483
[80] Hinze R,Jeuring J.Generic Haskell:Practice and Theory[M]∥Generic Programming 2003,LNCS 2793.Berlin:Springer-Verlag,2003:1-56
[81] Gibbons J.Datatypes-Generic Programming[M]∥Spring School on Datatype-Generic Programming,LNCS 4719.Berlin:Springer-Verlag,2007:1-71
[82] Ancona D,Lagorio G.Coinductive Type Systems for Object- Oriented Languages[M]∥ECOOP 2009,LNCS 5653.Berlin:Springer-Verlag,2009:2-26
[83] Bertot Y,Komendantskaya E.Inductive and Coinductive Com-ponents of Corecursive Functions in Coq[J].Electronic Notes in Theoretical Computer Science,2008,203(5):25-47
[84] Skillicorn D B.Categorical Data Types[M]∥Second Workshop on Abstract Models for Parallel Computation.Oxford University Press,1992
[85] Skillicorn D B.Questions and Answers about Categorical DataTypes[R].Technical Rreport,Queen’s University,Computing and Information Science.1994
[86] Skillicorn D B,Cai W.A Cost Calculus for Parallel FunctionalProgramming[J].Journal of Parallel and Distributed Computing,1995,28(1):65-83
[87] Banger C R,Skillicorn D B.Constructing Categorical Data Types[R].Research Reports,Canada:Queen’s University,1993
[88] SkilliCorn D B.Foundation of Parallel Programming[M].Cambridge International Series on Parallel Computation,1994
[89] Orchard D A,Bolingbroke M,Mycroft A.Ypnos:Declarative,Parallel Structured Grid Programming[C]∥Proc.of DAMP 2010.NY:ACM Press,2010:15-24

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!