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

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.