[Haskell-cafe] A use case for *real* existential types

[Andres Löh]

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