Announcing the availability of a new report titled The Constructor Calculus from http://www-staff.it.uts.edu.au/~cbj/Publications/constructors.ps The *constructor calculus* is a variant of the lambda-calculus that supports generic programming of functions for mapping, folding, equality, addition, etc. based on fresh approach to data types, their constructors, and pattern-matching. Its type system uses higher types to represent functors or, more precisely, data functors (like list X but not A->X). Aside from any general interest for readers of this list, there are some interesting open problems in the denotational semantics. Quantification over higher type variables and over kinds can be used to type polymorphic functions like mapping, e.g. map : forall a. forall X::a, Y::a, F::a->*. P(X->Y) -> FX -> FY where a is a kind variable (representing the number of sorts of data involved) X and Y are variable representing a tuple of types, F is a higher type variable representing a functor, and P is the finite product functor. The denotational semantics of functor polymorphism was addressed in an earlier system (Functorial ML, Jay,Bell\`e, Moggi, Journal of Functional Programming, 1998) but that of kind polymorphism has yet to be worked out. If F :: (*,*)->* is a data functor then its semantics could be a functor D x D -> D for some category D. More generally, a data functor of kind k -> * could be given by a functor D^k -> D What is the story when k is replaced by a variable a? What kind of category D has an object that represents the type scheme of map above? Perhap a self-enriched category is required. Has anyone considered self-enrichment in the effective topos? General comments, or suggestions about the denotational semantics are welcome. Yours, Barry Jay -- Associate Professor C.Barry Jay, Phone: (61 2) 9514 1814 Associate Dean (RPP), Faculty of IT www-staff.it.uts.edu.au/~cbj University of Technology, Sydney. CRICOS Provider 00099F 24-Jun-2002 12:52:45 -0300,7423;000000000000-00000000