[Haskell] Real life examples

[John Meacham]

On Wed, Nov 24, 2004 at 10:40:41PM +0000, Ben Rudiak-Gould wrote:
> John Meacham wrote:
> 
> >On Wed, Nov 24, 2004 at 02:40:52PM +0000, Ben Rudiak-Gould wrote:
> >
> >>But they can all be implemented with George Russell's library plus safe
> >>(pure) uses of unsafePerformIO.
> >
> >George Russell's library is precicly an invalid use of unsafePerformIO.
> >[...] hiding it in a module doesn't make it go away.
> 
> Yes it does. :-) If each Haskell environment ships with a correct 
> implementation of the library, then its interface is the only part that 
> matters. If the unsafePerformIO hack doesn't work in your new Haskell 
> compiler, you can replace it with some other magic that does work. It's 
> fine for the Haskell environment to hide impure magic behind a pure 
> interface -- that's what the language is all about.


That is exactly the problem we are trying to solve. coming up with a
sane 'magic' which interacts well with all the semantics and program
transforms we expect to be valid in a functional setting.

the problem is the unsafePerformIO newIORef is NOT pure. it is broken by
beta reduction among other things. This is precicely the problem, there
are valid uses of unsafePerformIO where they hide a stateful
implementation in a pure function, but global state is not one of them. 

There is a fundamental difference here between 'works because you have
proven referential transparency and purity hold despite the use of
unsafePerformIO' and 'works by accident' which is how george russel's
and all stateful libraries using unsafePerformIO in that way work now.
This is also why hiding it in a module does not help from a theoretical
point of view, there is nothing keeping a cross-module optimization from
propegating the 'unsoundness' everywhere throughout your program. So
while you are correct in saying it is okay for the haskell environment
to hide impure magic behind a pure interface, this is not an example of
that. 


Also, there is a reason ghc exports things like unboxed types and RULES
pragmas which no sane user should ever touch in theory, people need to
be able to do system-type programming. The haskell libraries are written
in haskell for example.  Declaring that such a useful thing as global
variables can only be implemented by the system in a magic library sort
of goes against that and is a step backwards. or at least sideways.  

        John


Tangent:

there is a logical truism that goes something vaugly like

'if 2 = 3 then I am king: the proof
being, assume I am not king then 2 = 3 and 2 = 2 which is a
contradiction therefore I must be king.' 

anyone know the actual eloquent formulation of this? 

It is just suposed to demonstrate that ANY contradiction anywhere makes
anything provable and disprovable in a logical system, demonstrating why
"just a little unsoundness" is not really an option... but my
formulation doesn't sound quite right, does anyone know the proper one?


-- 
John Meacham - ⑆repetae.net⑆john⑈