Journal of Functional Programming

Monadic encapsulation of effects: a revised approach (extended version)

E. MOGGI a1 1 and AMR SABRY a2 2
a1 DISI, University of Genova, via Dodecaneso 35, 16146 Genova, Italy
a2 Computer Science Department, Indiana University Bloomington, IN 47405, USA


Launchbury and Peyton Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification of Hindley-Milner's type system. Our first contribution is to propose a more natural encapsulation construct exploiting higher-order kinds, which achieves the same encapsulation effect, but avoids the ad hoc type parameter of the original proposal. The second contribution is a type safety result for encapsulation of strict state using both the original encapsulation construct and the newly introduced one. We establish this result in a more expressive context than the original proposal, namely in the context of the higher-order lambda-calculus. The third contribution is a type safety result for encapsulation of lazy state in the higher-order lambda-calculus. This result resolves an outstanding open problem on which previous proof attempts failed. In all cases, we formalize the intended implementations as simple big-step operational semantics on untyped terms, which capture interesting implementation details not captured by the reduction semantics proposed previously.


1 Research partially supported by MURST and ESPRIT WG APPSEM.

2 Worked started at the University of Oregon. Supported by the National Science Foundation under Grant No. CCR-9733088.