Brandon S. Allbery KF8NH wrote:
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.
What do you mean? I mean, in Clean, we may ask the following question: are all functions of type say forall a . Either (a -> *World -> a) String -> [*World] or Either (forall a . a -> *World -> a) String -> Maybe *World pure? In Haskell, the answer to any such question is unconditionally "yes" (unless you're hacking with unsafePerformIO and GHC internals like RealWorld# of course) even with plenty of appearances of the IO type constructor. But in Clean, functions may perform side effects, that's the only way to explain why the examples loop and loop' aren't the same. Regards, apfelmus