Title: Arity Polymorphism and Dependent Types
Abstract. 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 device a type system that can express this form of polymorphism. In a calculus like Functorial ML (of [JBM98]), instead of having one combinator map, one has a family of combinators map_n parametrized over natural numbers, while in a system like PolyP (of [JJ97]) there are restriction on the arity of datatype constructors. We propose a type system with a limited form of dependent types and inductive types, which supports arity polymorphism.