[Haskell] IO Regions in Haskell98

[oleg at pobox.com]

After an experiment with the simple IO regions, one can conclude that
the only implementation of the regions has to be complex. It seems
however that there is a Haskell98 implementation of IO regions. The
solution involves no higher-ranked types, and works both in GHC and
Hugs. The idea is trivial: given

> newtype Q = Q Handle
> newtype IOM a = IOM (IO a)
> qGetChar :: Q -> IOM Char
> withFile :: FilePath -> (Q -> IOM a) -> IOM a

we wish to assure that the handle Q never escapes, neither explicitly
nor implicitly. If the handle is incorporated into the result of
|withFile|, the type |Q| must be mentioned in that result. The only
computation that eliminates type |Q| is qGetChar; but the latter
introduces the type |IOM|. It follows then that if we make sure that
neither |IOM| nor |Q| appear in the type of the values produced by
|withFile|, our goal is achieved.

We can define our own type introspection typeclasses to check that a
particular type has no occurrences of |Q| or |IOM|. Luckily, the
Haskell standard library already has what we need: |Typeable|. There
are instances of |Typeable| defined for all standard types, and there
are ways for the users to extend that set. So, we just need to add the
constraint |Typeable| to the type of |withFile|, and we have solved
our problem.

That solution, although simple, has an inconvenience: to prevent the
user from defining their own Typeable instances for |Q| and |IOM|, we
have to hide the latter type constructors. That makes it impossible
to write explicit signatures for the IO-region-related functions. The
enclosed solution offers a simple refinement, which avoids that
inconvenience.

It should be pointed out that we statically prevent _any_ handle from
escaping |withFile|, regardless of its nesting label. It seems that
this restriction is acceptable; I couldn't think of any compelling
example why would one need to be able to return the handle of the
outer region (given that handle is already available in the outer
region).

If we attempt to leak the handle
> test2 = withFile "/etc/motd" (\q -> return q)

we get the type error:

ERROR "IORegions98Test.hs":22 - Unresolved top-level overloading
*** Binding             : test2
*** Outstanding context : Typeable (Q Z)

in Hugs or
IORegions98Test.hs:22:8:
    No instances for (Data.Typeable.Typeable1 Q,
		      Data.Typeable.Typeable IORegions98.Z)
      arising from use of `withFile'
    Probable fix:
      add an instance declaration for (Data.Typeable.Typeable1 Q,
				       Data.Typeable.Typeable IORegions98.Z)
   In the definition of `test2': test2 = withFile "/etc/motd" (\ q -> return q)

in GHC. It is easy to see that even a very trusting user cannot follow
the GHC advice and add the instance of Typeable for the type |Z|
because the latter is not available to the user of the library.

We get the similar errors for

> test4 = withFile "/etc/motd" (\q ->  return (qGetChar q))

ERROR "IORegions98Test.hs":26 - Unresolved top-level overloading
*** Binding             : test4
*** Outstanding context : Typeable (IOM Z Char)

and for Brandon Moore's test:

> test4' () = join $ withFile "/etc/motd" (\q ->  return (qGetChar q))

ERROR "IORegions98Test.hs":78 - 
Instance of Typeable (IOM Z Char) required for definition of test4'

The regular tests, e.g.,

> reader2 :: Q mark -> Q mark -> IOM mark String
> 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 = runIOM test5 >>= print

pass as before. We can give the explicit signature to our functions,
if we wish.

---- file IORegions98.hs
{-- Haskell98! --}

-- Even simpler IO Regions, in Haskell98

module IORegions98 (runIOM, qGetChar, withFile,
		    -- Only types are exported, not their data constructors
		    Q, IOM
		    ) where

import Control.Exception
import System.IO
import Data.Typeable

-- The marked IO monad. The data constructor is not exported.
-- Monad derivation is not supported in Haskell98, we have to do it by hand
-- newtype IOM marks a = IOM (IO a) deriving Monad
newtype IOM marks a = IOM (IO a)
unIOM (IOM x) = x
instance Monad (IOM marks) where
    return  = IOM . return
    m >>= f = IOM (unIOM m >>= unIOM . f)

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

-- The only mark that we use here. Even its type is not exported.
-- It is important that Z must NOT be the instance of Typeable
data Z = Zunused

-- Reading from a marked handle. The mark must be within the marks
-- associated with the IOM monad. We only use one mark:
-- since we prevent escaping of the Q handle from the inner scope,
-- the only handles in scope must be the ones created in the current
-- or outer regions.
qGetChar :: Q mark -> IOM mark Char
qGetChar (Q h) = IOM $ hGetChar h

-- There must not be an operation to close a marked handle!
-- withFile takes care of opening and closing (and disposing) of 
-- handles.
-- If one really must close the handle prematurely, throw any exception.
-- When the exception reaches withFile, the handle will be closed.
-- If the handle is to be closed, the rest of its region becomes useless
-- anyway.

-- Open the file, 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.
-- Because Z is not the instance of Typeable, and because Z is completely
-- hidden (so it cannot be made the instance of Typeable), neither
-- |Q Z| nor |IOM Z| may appear in |a|.

withFile :: Typeable a => FilePath -> (Q Z -> IOM Z a) -> IOM Z a
withFile filename proc = 
 IOM(
     bracket
     (openFile filename ReadMode)
     (hClose)
     (\handle -> unIOM $ proc (Q handle)))

-- Running the IOM monad
runIOM :: IOM Z a -> IO a
runIOM = unIOM


--- file IORegions98Test.hs
{-- Haskell98! --}

-- Simple IO Regions. Tests

module IORegions98Test where

import IORegions98
import Monad

reader q = do
	   c1 <- qGetChar q
	   c2 <- qGetChar q
	   return [c1,c2]

test0 = withFile "/etc/motd" (const $ return True)

test1  = withFile "/etc/motd" reader
test1r = runIOM test1 >>= print

-- An attempt to leak a handle
-- test2 = withFile "/etc/motd" (\q -> return q)
test3 = withFile "/etc/motd" (\q ->  (qGetChar q))

-- An attempt to leak a computation that uses the handle
-- test4 = withFile "/etc/motd" (\q ->  return (qGetChar q))

-- Dealing with two handles
-- Now we add the type signature, just to show that we can do that

reader2 :: Q mark -> Q mark -> IOM mark String
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 = runIOM test5 >>= print

-- An attempt to leak the handles.
{-
test6 = withFile "/etc/motd" 
	 (\q2 -> 
	  do
	  q' <- withFile "/etc/motd" (\q -> return q)
	  qGetChar q')


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

-}

-- An attempt to leak computations involving handles
{-
test8 = withFile "/etc/motd" 
	 (\q2 -> 
	  do
	  a <- withFile "/etc/motd" (\q -> return (qGetChar q))
	  a)

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

test9r = runIOM test9 >>= print
-}

-- An attempt to leak a computation that uses the handle, by Brandon Moore
--test4' () = join $ withFile "/etc/motd" (\q ->  return (qGetChar q))

--- file IORegions98Test1.hs
{-# OPTIONS -fglasgow-exts #-}

-- Simple IO Regions. Tests
-- Attempt to break the safety guarantees by using encapsulated polymorphic
-- types

module IORegions98Test1 where

import IORegions98
import Monad
import Data.Typeable

data W1 a = W1 (forall marks. IOM marks a)
data W2   = W2 (forall marks. Q marks)
data W3 a = W3 (forall marks. Q marks -> IOM marks a)

instance Typeable1 W1
-- Hugs likes the commented-out instance
--instance Typeable a => Typeable (W3 a)
instance Typeable1 W3
instance Typeable W2

--test1 = withFile "/etc/motd" (\q -> return $ W2 q)
--test2 = withFile "/etc/motd" (\q -> return $ W1 (qGetChar q))
test3 = withFile "/etc/motd" (\q -> return $ W3 (qGetChar))
--test4 = withFile "/etc/motd" (\q -> return $ W3 (\q1 -> qGetChar q))