Eugenio Moggi
Professor at DIBRIS, University of Genova
Categories (of Classes) for Collection Types
Abstract:
Collection types
have been proposed by Buneman and others (in the '90) as a way to
capture database query languages in a typed setting.
In 1998
Manes introduced the notion of collection monad on the category S of
sets as a suitable semantics for collection types. The canonical
example of collection monad is the finite powerset monad Pf.
In
order to account for the algorithmic aspects of database languages, the
category S is unsuitable, and should be replaced with other categories,
whose arrows are maps computable by "low complexity" algorithms.
We
propose "realizability for DSL" (Domain Specific Languages), where the
starting point is a monoid C of endomaps on a set D, instead of a
(partial) combinatory algebra on D, as a way to get such categories by
constructions like the category A[C] of "assemblies".
Interesting choices of C on the set N of natural numbers are: - N->N the set of all maps on N - R the set of primitive recursive maps - K the set of Kalmar elementary maps (level 3 in Grzegorczyk sub-recursive hierarchy).
In
them one can define an analogue of the finite powerset monad Pf and
recast the notion of collection monad. A systematic way to get Pf
is to borrow ideas from AST (Algebraic Set Theory, started by Joyal and
Moerdijk in the '90), where the key idea is to fix a notion of "small"
map in a category of "classes", and read "small" as "finite" (and
"large" as "countable").
By taking "small" maps as the key notion one can see other uses that are not directly related to collection types: -
models for fragments of Martin-Lof extensional type theory with a
universe of finite types (and define polynomials in the style of
Gambino and Kock); - non-standard models for AST by taking algebras Pf(U)->U for the functor Pf
Bio: Professor
Eugenio Moggi, MSc from Pisa (1983) and PhD from Edinburgh (1988), has
worked at the Univ. of Cambridge, Edinburgh and Pisa, before moving to
Genova in 1990.