constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A domain specific programming language is one designed for a specialized kind (“domain”) of applications. A domain specific embedded programming language (DSEL) is a domain specific language realized “inside” a general-purpose high level (typed) programming language.
There is at least some similarity between DSELs and synthetic mathematics, see for instance (Hudak 98, section 3.2). In (Hudak 98, figure 2) this shows aspects of a real-world DSL for “geometric region analysis” embedded in Haskell which under the relation between type theory and category theory/computational trinitarianism one immediately recognizes as a fragment of synthetic geometry.
Many existing quantum programming languages are actually domain-specific languages for the description of quantum circuits, and as such many are embedded in ambient type theories.
For instace:
Quipper is embedded into into Haskell [Green, Lumsdaine, Ross, Selinger & Valiron (2013)];
QWIRE has been embedded into Coq (Rand, Paykin & Zdancewic (2018)) and homotopy type theory [Paykin & Zdancewic (2019)].
CoqQ is another quantum programming language embedded in Coq [Ying et al. (2022)]
See also Rennela & Staton (2020) for more general discussion.
Discussion for embedding in Haskell:
A list of literature is at
Discussion specifically of quantum programming languages for quantum circuits as domain specific embedded languages:
Last revised on November 12, 2022 at 09:46:33. See the history of this page for a list of all contributions to it.