[Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)

[apfelmus]

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