domain specific embedded programming language in nLab
Context
Constructivism, Realizability, Computability
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
Constructive mathematics
Realizability
Computability
Contents
Idea
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.
Relation to synthetic mathematics
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.
Relation to monadic effects
There is a close relation between embedding a domain-specific language and declaring do-notation for monadic effects, see Benton, Hughes & Moggi 2002, §5.3 who write:
Every time a functional programmer designs a combinator library, then, we might as well say that he or she designs a domain specific programming language […]. This is a useful perspective, since it encourages programmers to produce a modular design, with a clean separation between the semantics of the DSL and the program that uses it, rather than mixing combinators and ‘raw’ semantics willy-nilly. And since monads appear so often in programming language semantics, it is hardly surprising that they appear often in combinator libraries also!
Examples
Quantum programming
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 instance:
-
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.
References
-
Paul Hudak, Building Domain-Specific Embedded Languages, ACM Computing Surveys 28 4e (1996) 196–es [doi:10.1145/242224.242477, web]
-
Paul Hudak, Modular Domain Specific Languages and Tools, in: Proceedings of Fifth International Conference on Software Reuse, IEEE Computer Society Press (1998) [pdf, doi:10.5555/551789.853532]
With emphasis on the relation to monads in computer science:
- Nick Benton, John Hughes, Eugenio Moggi, §5.3 in: Monads and Effects, in: Applied Semantics, Lecture Notes in Computer Science 2395, Springer (2002) 42-122 [doi:10.1007/3-540-45699-6_2]
Discussion for embedding in Haskell:
- HaskellWiki, Embedded domain specific language
A list of literature is at
- Haskell Wiki, Research papers/Domain specific languages
Discussion specifically of quantum programming languages for quantum circuits as domain specific embedded languages:
- Mathys Rennela, Sam Staton, Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory, Logical Methods in Computer Science 16 1 (2020) [arXiv:1711.05159, doi:10.23638/LMCS-16(1:30)2020]
Last revised on October 14, 2023 at 09:15:54. See the history of this page for a list of all contributions to it.