A unified approach to two previous lines of research based on the study of computational effects is presented in this paper. These lines are, respectively, the use of effect typing and the use of monads.
The first author conjectured as to whether a type inference similar to those used in effect systems could apply to a language based on monads. The conjecture is solved in this paper by providing a mixed approach, hence the word “marriage” in the title, using both effects and monads.
The authors use a particular type system--the type, region, and effect system of Talpin and Jouvelot--and introduce a corresponding type system for monads, together with a monad translation that is proven to preserve types. Later, operational semantics are introduced for both approaches, and it is proven that the translation preserves the semantics. Finally, type reconstruction algorithms are presented for the two approaches, and the translation is proven to relate both algorithms.
The results presented are all obtained using well-known techniques, although some minor technical problems arise when one examines the details of the proofs. This paper is, however, an interesting and important contribution, in that a firm mathematical foundation is linked to existing developments for the treatment of computational effects.