Modeling Quantum Computing Constraints: No-Cloning Theorem and Monadic Expressiveness with Type-Level Programming

• Flávio Borin Júnior UFSM
• Juliana Kaizer Vizzotto UFSM

DOI: https://doi.org/10.5753/sblp.2025.13218

Resumo

This paper presents a type-safe model of quantum computing, building upon the model introduced by Sabry in Haskell. By applying type-level programming techniques, we extend the model to constrain invalid operations and states at compile time. Our implementation enforces the no-cloning theorem at the type level via memory access patterns, while maintaining expressiveness via monadic composition of quantum operations. The implementation serves both as an introduction to quantum computing fundamentals and as a case study in enforcing physical constraints through a functional programming type system.

Palavras-chave: Type-Level Programming, Quantum Computing, Quantum Circuit Languages

Referências

T. Altenkirch and J. Grattage. 2005. A functional quantum programming language. In 20th Annual IEEE Symposium on Logic in Computer Science (LICS’ 05). 249–258. DOI: 10.1109/LICS.2005.1

André Berthiaume and Gilles Brassard. 1994. Oracle quantum computing. Journal of modern optics 41, 12 (1994), 2521–2535.

Liliane-Joy Dandy, Emmanuel Jeandel, and Vladimir Zamdzhiev. 2023. Type-safe Quantum Programming in Idris. In Programming Languages and Systems: 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings (Paris, France). Springer-Verlag, Berlin, Heidelberg, 507–534. DOI: 10.1007/978-3-031-30044-8_19

D. Deutsch. 1985. Quantum theory, the Church–Turing principle and the universal quantum computer. In Proc. R. Soc. Lond. 97–117. DOI: 10.1098/rspa.1985.0070

Richard A. Eisenberg and StephanieWeirich. 2012. Dependently typed programming with singletons. SIGPLAN Not. 47, 12, 117–130. DOI: 10.1145/2430532.2364522

John Hughes. 2005. Programming with Arrows. In Advanced Functional Programming, Varmo Vene and Tarmo Uustalu (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 73–129.

Sandy Maguire. 2019. Thinking with Types: Type-Level Programming in Haskell (1th ed.).

Michael A. Nielsen and Isaac L. Chuang. 2010. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press.

Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: a core language for quantum circuits. SIGPLAN Not. 52, 1 (Jan. 2017), 846–858. DOI: 10.1145/3093333.3009894

Amr Sabry. 2003. Modeling quantum computing in Haskell (Haskell ’03). Association for Computing Machinery, New York, NY, USA, 39–49. DOI: 10.1145/871895.871900

P.W. Shor. 1994. Algorithms for quantum computation: discrete logarithms and factoring. In Proceedings 35th Annual Symposium on Foundations of Computer Science. 124–134. DOI: 10.1109/SFCS.1994.365700

D.R. Simon. 1994. On the power of quantum computation. In Proceedings 35th Annual Symposium on Foundations of Computer Science. 116–123. DOI: 10.1109/SFCS.1994.365701

André van Tonder. 2004. A Lambda Calculus for Quantum Computation. SIAM J. Comput. 33, 5 (2004), 1109–1135. DOI: 10.1137/S0097539703432165

Andre van Tonder and Miquel Dorca. 2003. Quantum computation, categorical semantics and linear logic. (10 2003). arXiv:quant-ph/0312174

Juliana Vizzotto, Thorsten Altenkirch, and Amr Sabry. 2006. Structuring quantum effects: superoperators as arrows. Mathematical. Structures in Comp. Sci. 16, 3, 453–468. DOI: 10.1017/S0960129506005287