Hi.

So the natural question here is if we can employ the type system to enforce this correspondence. Phantom types immediately come to mind, as this problem is almost the same as ensuring that STRefs are only ever used in a single ST computation. The twist is that the inotify interface has nothing analogous to runST, which does the "heavy lifting" of the type magic behind the ST monad.

This twist is very simple to deal with if you have real existential types, with the relevant part of the interface looking approximately like

init :: exists a. IO (Inotify a) addWatch :: Inotify a -> FilePath -> IO (Watch a) rmWatch :: Inotify a -> Watch a -> IO ()

You can still do the ST-like encoding (after all, the ST typing trick is just an encoding of an existential), with init becoming "like runST":

init :: (forall a. Inotify a -> IO b) -> IO b addWatch :: Inotify a -> FilePath -> IO (Watch a) rmWatch :: Inotify a -> Watch a -> IO ()

Looking at your inotify.hs, the code of init becomes:

init :: (forall a. Inotify a -> IO b) -> IO b init k = do nextWatchRef_ <- newIORef 0 currentWatchesRef_ <- newIORef [] k $ Inotify { nextWatchRef = nextWatchRef_ , currentWatchesRef = currentWatchesRef_ }

And the code of main becomes:

main = init $ \ nd0 -> do wd0 <- addWatch nd0 "foo" wd1 <- addWatch nd0 "bar" init $ \ nd1 -> do wd3 <- addWatch nd1 "baz" printInotifyDesc nd0 printInotifyDesc nd1 rmWatch nd0 wd0 rmWatch nd1 wd3 -- These lines cause type errors: -- rmWatch nd1 wd0 -- rmWatch nd0 wd3 printInotifyDesc nd0 printInotifyDesc nd1

Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com

Maybe I understand the problem incorrectly, but it seems to me that you're overcomplicating things. With that kind of interface you don't actually need existential types. Or phantom types. You can just keep Inotify inside the Watch, like this: import Prelude hiding (init, map) import Data.IORef data Inotify = Inotify {nextWatchRef :: IORef Int, currentWatchesRef :: IORef [(Int,String)]} data Watch = Watch Int Inotify init ::IO Inotify init = do nextWatchRef_ <- newIORef 0 currentWatchesRef_ <- newIORef [] return Inotify { nextWatchRef = nextWatchRef_ , currentWatchesRef = currentWatchesRef_ } addWatch :: Inotify -> String -> IO Watch addWatch nd filepath = do wd <- readIORef (nextWatchRef nd) writeIORef (nextWatchRef nd) (wd + 1) map <- readIORef (currentWatchesRef nd) writeIORef (currentWatchesRef nd) ((wd,filepath):map) return (Watch wd nd) rmWatch :: Watch -> IO () rmWatch (Watch wd nd) = do map <- readIORef (currentWatchesRef nd) writeIORef (currentWatchesRef nd) (filter ((/= wd) . fst) map) printInotifyDesc :: Inotify -> IO () printInotifyDesc nd = print =<< readIORef (currentWatchesRef nd) main :: IO () main = do nd0 <- init wd0 <- addWatch nd0 "foo" _ <- addWatch nd0 "bar" nd1 <- init wd3 <- addWatch nd1 "baz" printInotifyDesc nd0 printInotifyDesc nd1 rmWatch wd0 rmWatch wd3 printInotifyDesc nd0 printInotifyDesc nd1 OK, I understand that it might be not what you want. For example, it could be that you can combine two different Watches if and only if they refer to the same Inotify. Well, then you need existential types. But you almost did it right, all you have to do now is to wrap Inotify in another type like that: {-# LANGUAGE ExistentialQuantification #-} import Prelude hiding (init, map) import Data.IORef data Inotify a = Inotify { nextWatchRef :: IORef Int , currentWatchesRef :: IORef [(Int,String)] } newtype Watch a = Watch Int data PolyInotify = forall a. PolyInotify (Inotify a) init :: IO PolyInotify init = do nextWatchRef_ <- newIORef 0 currentWatchesRef_ <- newIORef [] return $ PolyInotify Inotify { nextWatchRef = nextWatchRef_ , currentWatchesRef = currentWatchesRef_ } addWatch :: Inotify a -> String -> IO (Watch a) addWatch nd filepath = do wd <- readIORef (nextWatchRef nd) writeIORef (nextWatchRef nd) (wd + 1) map <- readIORef (currentWatchesRef nd) writeIORef (currentWatchesRef nd) ((wd,filepath):map) return (Watch wd) rmWatch :: Inotify a -> Watch a -> IO () rmWatch nd (Watch wd) = do map <- readIORef (currentWatchesRef nd) writeIORef (currentWatchesRef nd) (filter ((/= wd) . fst) map) printInotifyDesc :: Inotify a -> IO () printInotifyDesc nd = print =<< readIORef (currentWatchesRef nd) main :: IO () main = do pnd0 <- init case pnd0 of PolyInotify nd0 -> do wd0 <- addWatch nd0 "foo" _ <- addWatch nd0 "bar" pnd1 <- init case pnd1 of PolyInotify nd1 -> do wd3 <- addWatch nd1 "baz" printInotifyDesc nd0 printInotifyDesc nd1 rmWatch nd0 wd0 rmWatch nd1 wd3 -- These lines cause type errors: -- rmWatch nd1 wd0 -- rmWatch nd0 wd3 printInotifyDesc nd0 printInotifyDesc nd1 You may also choose to employ Rank2Types, which would make this more ST-like, with "init" playing the part of "runST": {-# LANGUAGE Rank2Types #-} import Prelude hiding (init, map) import Data.IORef data Inotify a = Inotify { nextWatchRef :: IORef Int , currentWatchesRef :: IORef [(Int,String)] } newtype Watch a = Watch Int init :: (forall a. Inotify a -> IO b) -> IO b init action = do nextWatchRef_ <- newIORef 0 currentWatchesRef_ <- newIORef [] action Inotify { nextWatchRef = nextWatchRef_ , currentWatchesRef = currentWatchesRef_ } addWatch :: Inotify a -> String -> IO (Watch a) addWatch nd filepath = do wd <- readIORef (nextWatchRef nd) writeIORef (nextWatchRef nd) (wd + 1) map <- readIORef (currentWatchesRef nd) writeIORef (currentWatchesRef nd) ((wd,filepath):map) return (Watch wd) rmWatch :: Inotify a -> Watch a -> IO () rmWatch nd (Watch wd) = do map <- readIORef (currentWatchesRef nd) writeIORef (currentWatchesRef nd) (filter ((/= wd) . fst) map) printInotifyDesc :: Inotify a -> IO () printInotifyDesc nd = print =<< readIORef (currentWatchesRef nd) main :: IO () main = init $ \nd0 -> do wd0 <- addWatch nd0 "foo" _ <- addWatch nd0 "bar" init $ \nd1 -> do wd3 <- addWatch nd1 "baz" printInotifyDesc nd0 printInotifyDesc nd1 rmWatch nd0 wd0 rmWatch nd1 wd3 -- These lines cause type errors: -- rmWatch nd1 wd0 -- rmWatch nd0 wd3 printInotifyDesc nd0 printInotifyDesc nd1 On May 10, 2013, at 2:17 PM, Leon Smith wrote:

I've been working on a new Haskell interface to the linux kernel's inotify system, which allows applications to subscribe to and be notified of filesystem events. An application first issues a system call that returns a file descriptor that notification events can be read from, and then issues further system calls to watch particular paths for events. These return a watch descriptor (which is just an integer) that can be used to unsubscribe from those events.

Now, of course an application can open multiple inotify descriptors, and when removing watch descriptors, you want to remove it from the same inotify descriptor that contains it; otherwise you run the risk of deleting a completely different watch descriptor.

So the natural question here is if we can employ the type system to enforce this correspondence. Phantom types immediately come to mind, as this problem is almost the same as ensuring that STRefs are only ever used in a single ST computation. The twist is that the inotify interface has nothing analogous to runST, which does the "heavy lifting" of the type magic behind the ST monad.

This twist is very simple to deal with if you have real existential types, with the relevant part of the interface looking approximately like

init :: exists a. IO (Inotify a) addWatch :: Inotify a -> FilePath -> IO (Watch a) rmWatch :: Inotify a -> Watch a -> IO ()

UHC supports this just fine, as demonstrated by a mockup attached to this email. However a solution for GHC is not obvious to me. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe