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

Launchbury and Peyton Jones came up with an ingenious idea for embedding re gions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification of Hindley-Milner's type s ystem. Our first contribution is to propose a more natural encapsulation co nstruct exploiting higher-order kinds, which achieves the same encapsulatio n effect, but avoids the ad hoe type parameter of the original proposal. Th e second contribution is a type safety result for encapsulation of strict s tate using both the original encapsulation construct and the newly introduc ed one. We establish this result in a more expressive context than the orig inal proposal, namely in the context of the higher-order lambda-calculus. T he third contribution is a type safety result for encapsulation of lazy sta te in the higher-order lamb da-calculus. This result resolves an outstandin g open problem on which previous proof attempts failed. In all cases, we fo rmalize the intended implementations as simple big-step operational semanti cs on untyped terms, which capture interesting implementation details not c aptured by the reduction semantics proposed previously.