Eugenio Moggi
Professor at DIBRIS, University of Genova

Categories (of Classes) for Collection Types

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

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.

Thursday, May, 8th, 2014
2:00 PM
Gates & Hillman Centers 8102

Principles of Programming Seminars