I am facing a situation that could be solved by ``defining a family of 
functors'', I describe the problem and would be very glad to get your 
views about it.

To illustrate the situation, I will suppose A1, ..., An are modules 
implementing the same signature S, let's say S contains the usual 
opertations on groups (mathematical groups, you can replace this by 
vector spaces, or whatever). It is easy to write a Product2 functor

Product2: A1:S -> A2:S -> S2

producing an implementation for the direct product (with signature S) of 
the groups A1 and A2, plus injections j1 : A1.t -> S2.t and j2: A2.t -> 
S2.t and corresponding projections (the type t denotes the module 
thingie, as usual). This extension of S is here written S2.

My problem is ``how do I remove the 2'' ? Would it be possible to define 
a functor scheme [:)]

Productn: A1:S -> .. -> An:S -> Sn

able to instantiate concrete functors for any value of n ?

It is possible to generate automatically appropriate code for small 
values of n, but I am looking for a better approach. It is simple to get 
close of the solution in the object paradigm, since I can simply put 
objects in an array and iterate over this array (IIRC this is the 
aggregate design pattern), but I do not see an easy way to define 
injections and projections.
-- 
Thanks for your suggestions,
Michaël