Simon Peyton-Jones wrote:

Previously I've thought of using a nested tuple type (m1, (m2, (m3 ())))

That was my thought too. But then we need the comparison operation on those 'm' (which are actually type eigen-variables). Not that it can't be done (it can, and several examples prove that). But it requires a little bit too many extensions. It appears there is a way to move the whole burden of maintaining the set of types (which become the set of constraints) to the typechecker. That is, to you...

Why do you need the instance IN () b ?

Don't we need at least one instance in a class so that the typechecker could resolve the constraint? Dominic Steinitz wrote:

Can someone give an explanation of how the marks get built up?

Suppose we have a class TypeEq a b so that the constraint TypeEq holds whenever a and b are the same. Then the type Int and the type TypeEq a Int => a are kind of equivalent, right? The HList library plays many tricks like that. The idea is that we can replace a definite type with a type variable subject to some constraint (which we can fix later on). In some respects, constraints are more convenient: they float, their order does not matter, their duplicates are automatically eliminated. Just what we need to build a set... It ``follows'' then that instead of building the union of types, we can build the union of constraints. The latter operation is trivial: the typechecker does that all the time. If we restrict the scope of the type variable by quantification, the scope of the corresponding constraint is likewise restricted. The quantification also builds eigen-variables (which are distinct from anything else) -- so we get 'gensym' on the type level for free. That is all there is to it... Chris Kuklewicz wrote:

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

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

As Andrew Pimlott has just pointed out on Haskell cafe, liftH functions should not be exported! The functions within the IORegions module have unrestricted access to the naked handle. They have to be careful and trusted: -- do not leak the unwrapped handle -- do not close the handle (if the handle really needs to be closed, one better just throw an exception or error) Because liftH accepts an _arbitrary_ function on handles, it essentially extends the trust to anyone outside of IORegions -- which defeats the latter's purpose. True, liftH functions are convenient -- but they must be used _inside_ of the module, to build qGetChar, qPutChar, etc. functions. It is the latter that can be exported. The idea of regions is that not all operations on handles are `safe'. Thus we need a way to specifically enumerate which are those primitive operations that safe. Enumerating lifted versions of getChar, putChar, etc. in the export list of IORegions is that enumeration. I'm afraid we have a circumstance where genericity is not a virtue.

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))

testMinus1 = join $ runIOM $ withFile "/etc/motd" $ return . runIOM . qGetChar

Isn't this the same situation we have in Haskell98 with respect to the regular IO? The safety of IO depends on the fact that the IO type constructor cannot be eliminated. Hence the 'main' trick, hence the only function that can eliminate IO is named 'unsafe'. If we wish for the safe runIOM, we have to enforce the same guarantees as we have in the ST monad regarding runST. That of course, cannot be done in Haskell98 (although the resulting library can be used in Haskell98 code). It should be emphasized that the Typeable constraint has reduced the problem of 'region nesting' to the regular problem of the 'linearity' of computations -- which is already solved in ST monad. We can add that pervasive 's' type parameter to our Q and IOM types. However, the simpler approach is just to use our 'mark' as that 's' parameter. So, the only changes are changes in the type signatures: withFile :: Typeable a => FilePath -> (Q mark -> IOM mark a) -> IOM mark a runIOM :: (forall mark. IOM mark a) -> IO a (and adding -fglasgow-exts flag, which is not-viral: the code that uses IO regions can remain Haskell98). Luckily, polymoprhic types, such as |IOM mark a| must be with respect to |mark|, cannot be instances of Typeable, so our safety constraint is automatically satisfied. I knew the polymorphic restriction on Typeable must be good for something.