Lazy IO and 'safe' uses of 'unsafePerformIO'

Matthias Mann mann at
Wed Oct 8 19:20:18 EDT 2003

Recently, there has been some discussion on this list about ongoing
research on the role of unsafePerformIO, lazy IO and evaluation
strategies. Within our research group at JWG-University Frankfurt some
work has been done concerning the development of a non-deterministic
call-by-need lambda calculus FUNDIO as a semantic basis for HasFuse, a
modified implementation of the Glasgow Haskell Compiler which compiles
Haskell programs using 'unsafePerformIO' in a 'safe' way, i.e. deploys
only those optimizations that have been proven correct w.r.t. FUNDIO. In
this context, experience with GHC's implementation has shown up that if
compiled with

    ghc -O0 -fno-do-lambda-eta-expansion

while avoiding INLINE-pragmas, 'most' uses of unsafePerfomIO are 'safe'
in the sense of FUNDIO's contextual equivalence. For further details,
downloads of papers and sources, please refer to the project WWW page

The results of FUNDIO show how evaluation may be interleaved with
direct-call IO. In particular not only

(\xs -> let z = length xs in "Hello World\n") _|_ = "Hello World\n"

is a valid equation in FUNDIO, but also for an arbitrary expression t
which may involve direct-call IO the equation

(\xs -> let z = length xs in "Hello World\n") t = "Hello World\n"

holds. Furthermore, the investigations indicate that some kind of
optimistic evaluation is possible, i.e. the expression t above could be
evaluated as long as no IO in t is executed. Hence, a demand-driven
style for IO could be achieved.

Matthias Mann
JWG-University Frankfurt

More information about the Haskell-Cafe mailing list