论文标题
一种分类编程语言
A Categorical Programming Language
论文作者
论文摘要
提出了基于类别理论的数据类型的理论。我们在F，G-Dialgebras的新分类概念下组织数据类型，这是辅助概念以及T-Elgebras的概念的扩展。 T-Elgebras也用于域理论，但是域理论一开始需要一些原始的数据类型，例如产品，但我们不需要任何东西。产物，副反应和指示（即功能空间）的定义与使用辅助的类别理论完全定义。 F，G-Dialgebras还使我们能够定义自然数对象，有限列表的对象以及编程中其他熟悉的数据类型。此外，它们的对称性使我们能够具有自然数对象的双重对象和无限列表（或懒惰列表）的对象。我们还使用F，G-Dialgebras作为其数据类型声明机制以分类样式引入一种编程语言。我们在操作上定义语言的含义，并证明任何程序都使用Tait的可计算方法终止。
A theory of data types based on category theory is presented. We organize data types under a new categorical notion of F,G-dialgebras which is an extension of the notion of adjunctions as well as that of T-algebras. T-algebras are also used in domain theory, but while domain theory needs some primitive data types, like products, to start with, we do not need any. Products, coproducts and exponentiations (i.e. function spaces) are defined exactly like in category theory using adjunctions. F,G-dialgebras also enable us to define the natural number object, the object for finite lists and other familiar data types in programming. Furthermore, their symmetry allows us to have the dual of the natural number object and the object for infinite lists (or lazy lists). We also introduce a programming language in a categorical style using F,G-dialgebras as its data type declaration mechanism. We define the meaning of the language operationally and prove that any program terminates using Tait's computability method.
