[Haskell-cafe] one-way monads

[Janis Voigtlaender]

Lauri Alanko wrote:
> On Tue, May 20, 2008 at 07:54:33AM +0200, Zsolt SZALAI wrote:
> 
>>Here comes IO and one-way monads, where the internal state can not be
>>extacted, and seems, that the internal data is global to the program.
>>Hows that could be? Is it just because main::IO() or because the
>>implementation of IO uses external C functions and there are no
>>internal state in the monad itself at all?
> 
> 
> There's nothing magical about the IO monad as a concept. It is true
> that it is handled specially by the library and the compiler, but this
> is just for performance reasons.
> 
> IO _could_ well be an ordinary datatype:
> 
> data IO a where
>   Return :: a -> IO a
>   Bind :: IO a -> (a -> IO b) -> IO b
>   OpenFile :: FilePath -> IOMode -> IO Handle
>   HPutChar :: Handle -> Char -> IO ()
>   HGetChar :: Handle -> IO Char
>   HClose :: Handle -> IO ()
>   -- etc.
> 
> If it were implemented like this, then the only magic would be in the
> runtime, which would take the IO value returned by the main function
> and somehow execute it. But if the implementation of IO were like
> this, and the datatype were exposed, then we could perfectly well
> write a userlevel "sandboxing" function:
> 
> runVirtual :: IO a -> VirtualWorld -> (a, VirtualWorld)
> 
> Where "VirtualWorld" would be a sandbox that contains all the state
> that IO operations can access: at least a filesystem, maybe something
> else too. This would probably count as "extraction".

In this context, the IOSpec library springs to mind:

http://www.cs.nott.ac.uk/~wss/repos/IOSpec/

-- 
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt at tcs.inf.tu-dresden.de