  Selinger gave a superoperator model of a first-order quantum programming
language and proved that it is fully definable and hence fully abstract. This
paper proposes an extension of the superoperator model to higher-order programs
based on modules over superoperators or, equivalently, enriched presheaves over
the category of superoperators. The enriched presheaf category can be easily
proved to be a model of intuitionistic linear logic with cofree exponential,
from which one can cave out a model of classical linear logic by a kind of
bi-orthogonality construction. Although the structures of an enriched presheaf
category are usually rather complex, a morphism in the classical model can be
expressed simply as a matrix of completely positive maps. The model inherits
many desirable properties from the superoperator model. A conceptually
interesting property is that our model has only a state whose "total
probability" is bounded by 1, i.e. does not have a state where true and false
each occur with probability 2/3. Another convenient property inherited from the
superoperator model is a $\omega$CPO-enrichment. Remarkably, our model has a
sufficient structure to interpret arbitrary recursive types by the standard
domain theoretic technique. We introduce Quantum FPC, a quantum
$\lambda$-calculus with recursive types, and prove that our model is a fully
abstract model of Quantum FPC.
