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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
