  We describe a type system for the linear-algebraic lambda-calculus. The type
system accounts for the part of the language emulating linear operators and
vectors, i.e. it is able to statically describe the linear combinations of
terms resulting from the reduction of programs. This gives rise to an original
type theory where types, in the same way as terms, can be superposed into
linear combinations. We show that the resulting typed lambda-calculus is
strongly normalizing and features a weak subject-reduction.
