The Type and Effect Discipline

AbstractThe type and effect discipline is a new framework for reconstructing the principal type and the minimal effect of expressions in implicitly typed polymorphic functional languages that support imperative constructs. The type and effect discipline outperforms other polymorphic type systems. Just as types abstract collections of concrete values, effects denote imperative operations on regions. Regions abstract sets of possibly aliased memory locations. Effects are used to control type generalization in the presence of imperative constructs while regions delimit observable side-effects. The observable effects of an expression range over the regions that are free in its type environment and its type; effects related to local data structures can be discarded during type reconstruction. The type of an expression can be generalized with respect to the type variables that are not free in the type environment or in the observable effect. Introducing the type and effect discipline, we define both a dynamic and a static semantics for an ML-like language and prove that they are consistently related. We present a reconstruction algorithm that computes the principal type and the minimal observable effect of expressions. We prove its correctness with respect to the static semantics