Computer Science Department
School of Computer Science, Carnegie Mellon University
Practical and Safe Abstractions for
Stefan K. Muller, William A. Duff, Umut A. Acar
We propose abstractions and techniques for interactive or reactive computation that are general-purpose, expressive, flexible, and that can enable writing efficient interactive programs. Our key interactivity abstraction is a factor: a co-inductive type that abstracts interaction as exchange of information and internal state change. To enable expressive and flexible development of interactive programs, we extend a linearly typed, call-by-value lambda calculus with factors as first-class values. The resulting language, called λi, allows input and output through factors that reflect the changing state of the world. To ensure correctness and efficiency in the presence of such effects, λi treats interaction as a consumable, linear resource. The small-step semantics of λi takes advantage of the linearity to prevent unsafe behavior as well as guarantee efficiency. We formalize λi, and establish its type safety and additional meta-theoretical results that show that interaction and purely functional programming are not always inconsistent. We formalize all of our results in the Coq proof assistant. We give an implementation of λi as an OCaml library along with a relatively broad range of example applications.