On Fri, 2007-11-02 at 08:35 -0400, Brandon S. Allbery KF8NH wrote:
On Nov 2, 2007, at 6:35 , apfelmus wrote:
during function evaluation. Then, we'd need a "purity lemma" that states that any function not involving the type *World as in- and output is indeed pure, which may be a bit tricky to prove in the presence of higher-order functions and polymorphism. I mean, the function arrows are "tagged" for side effects in a strange way, namely by looking like *World -> ... -> (*World, ...).
I don't quite see that; the Clean way looks rather suspiciously like my "unwrapped I/O in GHC" example from a couple weeks ago, so I have trouble seeing where any difficulty involving functions not using *World / RealWorld# creeps in.
I will grant that hiding *World / RealWorld# inside IO is cleaner from a practical standpoint, though. Just not from a semantic one.
On the contrary. GHC's IO newtype isn't an implementation of IO in Haskell at all. It's an implementation in a language that has a Haskell-compatible subset, but that also has semantically bad constructs like unsafePerformIO and unsafeInterleaveIO that give side effects to operations of pure, non-RealWorld#-involving types. Clean's type system is specified in a way that eliminates both functions from the language, which recovers purity. But proving that is harder than I'd like to attempt. jcc