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

[MigMit]

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 <leon.p.smith at gmail.com> 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.
> <inotify.hs>_______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe