Linear usage of state
From MaRDI portal
categorical semanticscomputational effectsenriched category theorylinear type theorymonadsstate passing translation
Proof-theoretic aspects of linear logic and other substructural logics (03F52) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Categorical semantics of formal languages (18C50) Functional programming and lambda calculus (68N18)
Abstract: We investigate the phenomenon that "every monad is a linear state monad". We do this by studying a fully-complete state-passing translation from an impure call-by-value language to a new linear type theory: the enriched call-by-value calculus. The results are not specific to store, but can be applied to any computational effect expressible using algebraic operations, even to effects that are not usually thought of as stateful. There is a bijective correspondence between generic effects in the source language and state access operations in the enriched call-by-value calculus. From the perspective of categorical models, the enriched call-by-value calculus suggests a refinement of the traditional Kleisli models of effectful call-by-value languages. The new models can be understood as enriched adjunctions.
Recommendations
Cited in
(19)- Classical control and quantum circuits in enriched category theory
- Stateful runners of effectful computations
- Commutative semantics for probabilistic programming
- Linearly-used state in models of call-by-value
- Linear-use CPS translations in the enriched effect calculus
- Enriching an Effect Calculus with Linear Types
- Runners in Action
- The costructure–cosemantics adjunction for comodels for computational effects
- Classical control, quantum circuits and linear logic in enriched category theory
- Stream processors and comodels
- Sound and complete equational reasoning over comodels
- LNL polycategories and doctrines of linear logic
- Promonads and String Diagrams for Effectful Categories
- Sweedler theory of monads
- Q\# as a quantum algorithmic language
- Comodule representations of second-order functionals
- String diagrams for premonoidal categories
- Premonoidal and Kleisli double categories
- State-dependent SSB utility
This page was built for publication: Linear usage of state
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408192)
