Substitution, jumps, and algebraic effects
Loading...
Date
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Association for Computing Machinery (ACM)
https://doi.org/10.1145/2603088.2603163
https://doi.org/10.1145/2603088.2603163
Abstract
Description
Algebraic structures abound in programming languages. The starting point for this paper is the following theorem: (first-order) algebraic signatures can themselves be described as free algebras for a (second-order) algebraic theory of substitution. Transporting this to the realm of programming languages, we investigate a computational metalanguage based on the theory of substitution, demonstrating that substituting corresponds to jumping in an abstract machine. We use the theorem to give an interpretation of a programming language with arbitrary algebraic effects into the metalanguage with substitution/jumps.