Effect systems with subtyping

Effect systems extend classical type systems with effect information. Just as types describe the possible values of expressions, effects describe their possible evaluation behaviors. Effects, which appear in function types, int reduce new constraints on the typability of expressions. To increase the flexibility and accuracy of effect systems, we present a new effect system based on subtyping. The subtype relation is induced by a subsumption relation on effects. This w-At yping efjects ys t em avoids merging effect information t oget her, thus collecting more precise effect information. We introduce a reconstruction algorithm which for any expression already typed with classical types, reconstructs its type and effect based on the subtype relation. The reconstruction algorithm is sound and complete w .r.t. the static semantics.