И обозвали они это - "Constructive Category Theory".
Ещё советую почитать работу Hagino. "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 are defined exactly like in category theory using adjunctions. F,G-dialgebras also enable us to define natural number object, object for finite lists and other familiar data types in programming. Futhermore, 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 functional programming language in a categorical style. It has no primitive data types nor primitive control structures. Data types are declared using F,G-dialgebras and each data type is associated with its own control structure. For example, natural numbers are associated with primitive recursion. A specification language to describe categories is also included. It is used to give a formal semantics to F,G-dialgebras as well as to give a basis to the categorical programming language we introduce."
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2008-01-23 04:02 pm (UTC)"Constructive Category Theory".
Ещё советую почитать работу Hagino.
"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
are defined exactly like in category theory
using adjunctions. F,G-dialgebras also enable us
to define natural number object, object for
finite lists and other familiar data types in programming.
Futhermore, 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 functional programming language
in a categorical style. It has no primitive data types
nor primitive control structures. Data types are declared
using F,G-dialgebras and each data type is associated
with its own control structure. For example, natural numbers
are associated with primitive recursion.
A specification language to describe categories is also included.
It is used to give a formal semantics to F,G-dialgebras
as well as to give a basis to the categorical
programming language we introduce."
Не хватает только развитого полиморфизма,
ну и Зависимых Типов, но надо обратить внимание,
что год публикации - 1987.
Страничка Tatsuya Hagino -
http://www.tom.sfc.keio.ac.jp/~hagino/
Ссылка на книжку (там же) -
http://www.tom.sfc.keio.ac.jp/~hagino/thesis.pdf