Types and Effects Towards the Integration of Functional and Imperative Programming

摘要

We propose a new class of programming languages in which every expression has both a type and an effect: the type describes what sort of value the expression may return, and the effect describes what sort of side-effects the expression may have. Effects are described in terms of regions, which describe what part of the state of the computation may be affected. We show how the type system of the second-order lambda-calculus can be generalized to incorporate effect and region specifications. This leads to polymorphism with respect to types, effects, and regions. Our type and effect system makes it possible to embed functional program fragments within imperative programs, and vice versa, while retaining the benefits of the chosen programming style in each program fragment. The type and effect system can also be used to verify the encapsulation invariant of a monitored data type. It also offers a clean solution to the problem of first-class polymorphism in an imperative language. To test our ideas, we have designed a small imperative higher-order language called MFX, and we have implemented a compiler that analyzes MFX programs and translates them into dataflow graphs. Our long-term objective is the integration of functional and imperative programming into a single programming model that retains the benefits of both programming styles.