DSSE:2012 Academic Year Seminars
State Passing Style
Speaker(s): Sam Staton (University of Cambridge)
An imperative program of type X -> Y can often be written as a pure functional program in the state passing style, S*X -> S*Y (for a state type S). This makes the changing state explicit.
I will investigate the idea that EVERY computational effect can be treated in the state passing style. I will do this in the context of a metalanguage in which we can enforce the linear use of state: the state cannot be duplicated or discarded. Models of this metalanguage are enriched categories of a certain kind.
This is joint work with Rasmus Møgelberg, building on work by Jeff Egger and Alex Simpson.