[Haskell] Simple IO Regions

[Chris Kuklewicz]

I tweaked the IORegions code using some other ideas from the thread.

The "IOM marks a" monad which wrapped (IO a) is now "IOQ marks m a"
which wraps "m a".  So it is a MonadTrans and if m is MonadIO then so is
"IOQ marks m".

qGetChar was just a demo, and has been replaced by liftH, liftH2, and
liftH3 which should cover all the System.IO hFoo functions.

But bracket does not know what MonadIO is, so the withFile* functions
are no as general as possible.

Eventually these could be stuck on the wiki.

-- 
Chris

-------------- next part --------------
> {-# OPTIONS -fglasgow-exts #-}

This is a tweaked version from oleg.  I think all the "should not
compile" tests still correctly create error messages when compiled.

>
> module IORegionsTest where
>
> import IORegions3 -- see below
> import System.IO
>
> test0 = withFile "/etc/motd" (const $ return True)

With IORegions3, liftH,liftH2,liftH3 are exported, and withFile*
functions.  This lets us promote every h* functions ourselves. A
fseparate sub-module, perhaps IORegions.IO, could have all these
trivial lifting already written and named:

> qGetChar q = liftH hGetChar q
>
>
> reader q = do
> 	     c1 <- qGetChar q
> 	     c2 <- qGetChar q
> 	     return [c1,c2]
>
> test1 = withFile "/etc/motd" reader
> test1r = runIOQ test1 >>= print

Instead of handles, we have Qs -- marked handles. The are created by
the function withFile and used similar to regular handles. A special
IOQ monad is a newtype away from the regular IO. The phantom type
parameter of the IOQ monad maintains the marks of the regions.

	*IORegionsTest> :t reader
	reader :: (Monad (IOQ marks), IORegions.IN mark marks) =>
		  Q mark -> IOQ marks [Char]

the type of the reader shows that it takes a marked handle and yields
a marked IO computation. The constraint IN assures that the
computation must be marked with the mark of the handle.

If we attempt to leak the handle:
*> test2 = withFile "/tmp/i.hs" (\q -> return q)

we get
    Inferred type is less polymorphic than expected
      Quantified type variable `mark' escapes
    In the second argument of `withFile', namely `(\ q -> return q)'

The following is OK: we perform the computation and return its result:

> test3 = withFile "/etc/motd" (\q ->  (qGetChar q))
>
> test3r = runIOQ test3 >>= print

If we attempt to return the unperformed computation itself:
*> test4 = withFile "/tmp/i.hs" (\q ->  return (qGetChar q))

we get
    Could not deduce (IORegions.IN mark marks1)
      from the context (IORegions.IN mark marks)
      arising from use of `qGetChar' at IORegionsTest.h...

As we said earlier, more than one handle can be at play at the same
time:

> reader2 q1 q2 = do
> 	   c1 <- qGetChar q1
> 	   c2 <- qGetChar q2
> 	   return [c1,c2]
> test5 = withFile "/etc/motd" (\q1 -> 
> 			        withFile "/etc/motd" (\q2 -> reader2 q1 q2))
>
> test5r = runIOQ test5 >>= print

Incidentally, the inferred type of reader2 is

	*IORegionsTest> :t reader2
	reader2 :: (Monad (IOQ marks),
		    IORegions.IN mark1 marks,
		    IORegions.IN mark marks) =>
		   Q mark -> Q mark1 -> IOQ marks [Char]

Obviously, the resulting computation is marked with the marks of both
argument handles.

With two handles, we can actually return a handle -- provided we
return an outermost handle from the innermost region (but not the
other way around). For example, the following is wrong

*> test6 = withFile "/etc/motd" 
*> 	    (\q2 -> 
*> 	     do
*> 	     q' <- withFile "/etc/motd" (\q -> return q)
*> 	     qGetChar q')


but the following is OK:

> test7 = withFile "/etc/motd" 
> 	   (\q2 -> 
> 	    do
> 	    q' <- withFile "/etc/motd" (\q -> return q2)
> 	    qGetChar q')
>
> test7r = runIOQ test7 >>= print

Ditto for the computation:

The following is the improper leakage and leads to a type error:

*> test8 = withFile "/etc/motd" 
*> 	    (\q2 -> 
*> 	     do
*> 	     a <- withFile "/etc/motd" (\q -> return (qGetChar q))
*> 	     a)

But the following is fine:

> test9 = withFile "/etc/motd" 
>          (\q2 -> 
>           do
>           a <- withFile "/etc/motd" (\q -> return (qGetChar q2))
>           a)
>
> test9r = runIOQ test9 >>= print

All the test runners:

> tests = [test1r,test3r,test5r,test7r,test9r]
>
> runTests = sequence tests
-------------- next part --------------
{-# OPTIONS -fglasgow-exts #-}
{- 
  Version 2006-01-19 by Chris Kuklewicz

  This is a tweaked version from oleg, using Benjamin's phantom Mark
  instead of ().  And the monad was generalized from IO to any monad,
  allowing it to be a MonadTrans, and if it is over MonadIO (e.g. IO)
  then IOQ is a MonadIO as well. Instead of qGetChar, I made the three
  liftH* functions which can be applied to any handle h* function in
  System.IO (possibly in a sub-module of this one).

  But since there is no "unlift" operation, the withFile bracket code
  requires the procedure to be "IOQ marks IO a" over the IO monad.
  Error handling will run into similar restrictions.  I did generalize
  the withFile to take a FileMode, and provide IO and MonadIO
  instances (which helps with type inference when using this module).

  The IOM monad was renamed to IOQ since I altered its kind.

-}
module IORegions4 (runIOQ, withFile, withFileIO, withFileMode, liftH, liftH2, liftH3,
		  -- Only types are exported, not their data constructors!
		  QHandle, IOQ) where

import Control.Monad
import Control.Monad.Trans
import Control.Exception
import System.IO

-- The marked monad transformer. The data constructor is not exported.
-- The type 'marks' is purely phantom (and is never instantiated, actually)
newtype IOQ marks m a =  IOQ (m a) deriving (Monad)

instance MonadTrans (IOQ marks) where lift = IOQ
instance (MonadIO m) => MonadIO (IOQ marks m) where liftIO = IOQ . liftIO

-- This an unsafe operation to export
unIOQ :: IOQ mark m a -> m a
unIOQ (IOQ x) = x

-- Running the IOQ monad, type is different than unIOQ and safe to export
runIOQ :: (forall mark. IOQ mark m a) -> m a
runIOQ = unIOQ

-- The marked IO handle. The data constructor is not exported.
newtype QHandle mark = Q Handle

-- |IN mark marks| asserts that |mark| is a member of the mark set |marks|
-- The mark set is really a set, and the best of all, it's typechecker
-- that maintains it. We don't need to do anything at all.
class IN a b

-- |Mark| is the only (phantom) type that can be an instance of IN
data Mark
instance IN Mark

-- Wrap a handle as a marked handle
mark :: Handle -> QHandle Mark
mark h = Q h

-- Operating on a marked handle. The mark must be within the marks
-- associated with the IOQ monad

liftH :: (MonadIO m,IN mark marks) => (Handle -> IO a) -> QHandle mark -> IOQ marks m a
liftH op (Q h) = IOQ (liftIO (op h))

liftH2 :: (MonadIO m,IN mark marks) => (Handle -> x2 -> IO a) -> QHandle mark -> x2 -> IOQ marks m a
liftH2 op (Q h) x2 = IOQ (liftIO (op h x2))

liftH3 :: (MonadIO m,IN mark marks) => (Handle -> x2 -> x3 -> IO a) -> QHandle mark -> x2 -> x3 -> IOQ marks m a
liftH3 op (Q h) x2 x3 = IOQ (liftIO (op h x2 x3))

--qGetChar :: (MonadIO io, IN mark marks) => Q mark -> IOQ marks io Char -- is inferred
qGetChar q = liftH hGetChar q

-- There must not be an operation to close a marked handle!  withFile
-- takes care of opening and closing (and disposing) of handles.

-- Open the file, add the markset constraint for the duration of the
-- body, and make sure the marked handle does not escape.

-- The marked handle is closed on normal or abnormal exit from the
-- body

-- The type system guarantees the strong lexical scoping of
-- withFile. That is, we can assuredly close all the handles after we
-- leave withFile because we are assured that no computations with
-- marked handles can occur after we leave withFile.

withFile :: FilePath -> (forall mark. IN mark marks => QHandle mark -> IOQ marks IO a) -> IOQ marks IO a
withFile filename proc = IOQ
    (bracket
     (openFile filename ReadMode)
     (hClose)
     (\handle -> unIOQ $ proc $ mark handle))

withFileIO :: (MonadIO io) => FilePath -> (forall mark. IN mark marks => QHandle mark -> IOQ marks IO a) -> IOQ marks io a
withFileIO filename proc = IOQ $ liftIO
    (bracket
     (openFile filename ReadMode)
     (hClose)
     (\handle -> unIOQ $ proc $ mark handle))

withFileMode :: (MonadIO io) => FilePath -> IOMode -> (forall mark. IN mark marks => QHandle mark -> IOQ marks IO a) -> IOQ marks io a
withFileMode filename mode proc = IOQ $ liftIO
    (bracket
     (openFile filename mode)
     (hClose)
     (\handle -> unIOQ $ proc $ mark handle))

withFileModeIO :: FilePath -> IOMode -> (forall mark. IN mark marks => QHandle mark -> IOQ marks IO a) -> IOQ marks IO a
withFileModeIO filename mode proc = IOQ
    (bracket
     (openFile filename mode)
     (hClose)
     (\handle -> unIOQ $ proc $ mark handle))