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:
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.