Lazy IO and 'safe' uses of 'unsafePerformIO'
mann at ki.informatik.uni-frankfurt.de
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
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.
More information about the Haskell-Cafe