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

[Jonathan Cast]

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