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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
