ABOUT CONSTRUCTIVE VECTORS.

Let be E a given set.  In computer science, a usual name for the
elements of E x E x ...x E is vector.  For a fixed dimension, the
construction is easy, but, for any dimension, no generic construction
exists.  If one uses classical inductive constructions, like lists,
one is lead to put vectors of different dimensions in the same set,
whereas operations on vectors require to be defined on vectors of the
same dimension.  In this talk, I will present a definition that uses a
type dependant on the dimension and I will discuss the advantages and
drawbacks of such a definition.  Briefly, the constructed objects
model correctly vectors, but manipulating that kind of object is
slightly more complex than manipulating those of simple inductive
types.