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

Leon Smith leon.p.smith at gmail.com
Fri May 10 12:17:52 CEST 2013


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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130510/8fb73c57/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: inotify.hs
Type: application/octet-stream
Size: 1295 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130510/8fb73c57/attachment.obj>


More information about the Haskell-Cafe mailing list