On Circuit Description Languages, Indexed Monads, and Resource Analysis
Ken Sakayori, Andrea Colledan, Ugo Dal Lago
TL;DR
The paper develops a denotational semantics for circuit description languages in the Proto-Quipper family by modeling circuit construction as an indexed monad, thereby separating the produced circuit from the computed value. It introduces Proto-Quipper-C with closure-like arrow types, a monadic semantic framework via a parameterized Freyd category, and an effect system built on circuit algebras to quantify circuit size and metrics. The approach yields soundness and adequacy results and provides a unified, extensible way to reason about circuit metrics including optimization. It also discusses extensions to dependent types and departs from presheaf-based readings to enable modular, intensional circuit analysis with potential tool support for automation.
Abstract
In this paper, a monad-based denotational model is introduced and shown adequate for the Proto-Quipper family of calculi, themselves being idealized versions of the Quipper programming language. The use of a monadic approach allows us to separate the value to which a term reduces from the circuit that the term itself produces as a side effect. In turn, this enables the denotational interpretation and validation of rich type systems in which the size of the produced circuit can be controlled. Notably, the proposed semantic framework, through the novel concept of circuit algebra, suggests forms of effect typing guaranteeing quantitative properties about the resulting circuit, even in presence of optimizations.