We try to present, in this poster, an ongoing work on extending type systems for a programming language for quantum channels with duplicable and inductive data types. We define and formalize a programming language for description of interleaved quantum computation with classical computation, which is called quantum channel. In our basic type systems, each data is safely assumed to be linear, meaning that it can be used exactly once, to guarantee that the program does not violate some properties of quantum mechanics.

However, since classical data can be useful in classical computation, we need to incorporate classical data in our language. This leads us to our first goal for which we introduce duplicable data types in terms of bang (!) modality.

Still our basic type system is weak since there is no inductive data types. As an example, we attempt to introduce type for list. Then the type systems need to be able to reason about the shape of the list, which is the size.

There exist works on type systems for quantum circuit description language even more expressive than the type system we aim. These type systems contain recursive types and classical data types. However, our work is novel since we apply these works to a programming language for generalized quantum circuits.