Application - Haskell
|John Launchbury and Simon L Peyton Jones, (1995)
State in Haskell.
Abstract: Some algorithms make critical internal use of updatable state, even though their external specification is purely functional. Based on earlier work on monads, we present a way of securely encapsulating stateful computations that manipulate multiple, named, mutable objects, in the context of a non-strict, purely-functional language. The security of the encapsulation is assured by the type system, using parametricity. The same framework is also used to handle input/output operations (state changes on the external world) and calls to C.
|E.Moggi and F.Palumb, (1995)
Monadic Encapsulation of Eects: a Revised Approach (Extended Version).
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 modication of Hindley-Milner's type system. Our rst contribution is to propose a more natural encapsulation construct exploiting higher-order kinds, which achieves the same encapsulation eect, but avoids the bogus type parameter of the original proposal. The second contribution is a stronger type safety result, namely encapsulation of strict state in higherorder lambda-calculus. We formalise the intended implementation as a very simple big-step operational semantics on untyped terms, which captures interesting implementation details not captured by the reduction semantics proposed previously.
|Manfred Schmidt-schauß, J.W. GoetheUniversität Frankfurt, (Sep 2003).
FUNDIO: A Lambda-Calculus with a letrec, case, Constructors, and an IO-Interface: Approaching a Theory of unsafePerformIO.
Abstract: This paper proposes a non-standard way to combine lazy functional languages with I/O. In order to demonstrate the usefulness of the approach, a tiny lazy functional core language “FUNDIO”, which is also a call-by-need lambda calculus, is investigated. The syntax of “FUNDIO ” has case, letrec, constructors and an IO-interface: its operational semantics is described by small-step reductions. A contextual approximation and equivalence depending on the input-output behavior of normal order reduction sequences is defined and a context lemma is proved. This enables to study a semantics of “FUNDIO ” and its semantic properties. The paper demonstrates that the technique of complete reduction diagrams enables to show a considerable set of program transformations to be correct. Several optimizations of evaluation are given, including strictness optimizations and an abstract machine, and shown to be correct w.r.t. contextual equivalence. Correctness of strictness optimizations.
A call-by-need lambda calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations
A family of syntactic logical relations for the semantics of Haskell-like languages