Lazy IO and 'safe' uses of 'unsafePerformIO'

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
participants (1)
-
Matthias Mann