Hostname: page-component-7c8c6479df-5xszh Total loading time: 0 Render date: 2024-03-28T13:53:23.673Z Has data issue: false hasContentIssue false

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

Published online by Cambridge University Press:  28 November 2001

E. MOGGI
Affiliation:
DISI, University of Genova, via Dodecaneso 35, 16146 Genova, Italy
AMR SABRY
Affiliation:
Computer Science Department, Indiana University Bloomington, IN 47405, USA
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Research Article
Copyright
© 2001 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.