TAC abstracs

Abstracts

On algebraically exact categories and essential localizations of varieties spaces Algebraically exact categories have been introduced by Adamek, Lawvere and Rosicky as an equational hull of the 2-category of all varieties of finitary algebras. Our main result is the following representation theorem for algebraically exact categories:

a cocomplete category is algebraically exact and has a regular generator iff it is an essential localization of a variety.

This theorem is a further step in the non-additive generalization of some fundamental theorems in commutative algebra:

Lawvere characterization of varieties is the non-additive extension of the Gabriel-Mitchell characterization of module categories;
Popesco-Gabriel representation of Grothendieck categories has been extended to a non-additive context using the exact completion of a weakly left exact category;
our main result is the non-additive generalization of Roos characterization of essential localizations of module categories.

In a similar way, we also characterize essential localizations of presheaf categories.
This is joint work with J. Adamek and J. Rosicky.

Arity Polymorphism and Dependent Types In polytypic programming one would like to define combinators, such as map, which operate on datatype constructors of any arity. However, it is rather problematic to devise a type system that can express this form of polymorphism. In a calculus like Functorial ML, instead of having one combinator map, one has a family of combinators map_n parametrized over natural numbers, while in a system like PolyP there are restriction on the arity of datatype constructors. The most natural typing for the map combinator would be

Forall n:N. Forall F:Functor(n). Forall X,Y:Type^n.
  [ Forall i:n. X_i -> Y_i ] -> F(X) -> F(Y)

where n ranges over arities (say the numbers), F over functors of arity n, X and Y over n-tuples of types, and i over indices for arity n (e.g. the predecessors of n). We propose a type system with a limited form of dependent types and inductive types, which supports arity polymorphism.