[Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why
can't Haskell be faster?)
apfelmus at quantentunnel.de
Fri Nov 2 11:09:00 EDT 2007
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]
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.
More information about the Haskell-Cafe