Lazy IO and 'safe' uses of 'unsafePerformIO'

[Matthias Mann]

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

    http://www.ki.informatik.uni-frankfurt.de/research/diamond


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