Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1017/S0956796801004154 | J. Funct. Program. |
Keywords | Field | DocType |
extended version,original proposal,encapsulation effect,monadic encapsulation,natural encapsulation,original encapsulation,higher-order kind,type safety result,expressive context,type system,type parameter,higher-order lambda-calculus,revised approach,type safety,functional language,higher order,lambda calculus,operational semantics | Operational semantics,Programming language,Open problem,Functional programming,Computer science,Imperative programming,Theoretical computer science,Haskell,Type safety,Monad (functional programming),Semantics | Journal |
Volume | Issue | ISSN |
11 | 6 | 0956-7968 |
Citations | PageRank | References |
19 | 1.09 | 26 |
Authors | ||
2 | ||