Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages should also support quantum circuits as first-class citizens, as well as families of circuits that are indexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This paper defines a general semantic structure for such a type theory via certain fibrations of monoidal categories. The categorical model of the quantum circuit description language Proto-Quipper-M by Rios and Selinger (2017) constitutes an example of such a fibration, which means that the language can readily be integrated with dependent types. We then devise both a general linear dependent type system and a dependently typed extension of Proto-Quipper-M, and provide them with operational semantics as well as a prototype implementation.
翻译:现代量子编程语言结合量子资源和古典控制。 一方面, 它们必须是线性打字, 以反映量子资源的无线属性。 另一方面, 高水平和实用语言也应该支持量子电路作为一流公民, 以及按某些古典参数编制索引的电路组。 因此, 量子编程语言需要线性依附型式理论。 本文通过某些单项类别裂痕界定了这种类型理论的一般语义结构。 里约斯和塞林格尔( 2017) 的量子电路描述语言Proto- Quipper- M( 2017) 绝对模型是这种拼写法的一个例子, 这意味着该语言很容易与依附类型融合。 然后我们设计一个一般的线性依赖型类型系统和一个依附型的Proto- Quipper- M( Proto- Quipper- M) 扩展, 并为他们提供操作的语义学和原型执行。