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

[Leon Smith]

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.

[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

_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[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

> <inotify.hs>_______________________________________________

[Leon Smith]

On Fri, May 10, 2013 at 9:00 AM, Andres Löh <and...@well-typed.com> wrote:

> 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 ()

Right, but my interface the Inotify descriptor has an indefinite extent,  whereas your interface enforces a dynamic extent.   I'm not sure to what degree this would impact use cases of this particular library,  but in general moving a client program from the the first interface to the second can require significant changes to the structure of the program,   whereas moving a client program from the second interface to the first is trivial.    So I'd say my interface is more expressive.

Best,
Leon

[Leon Smith]

On Fri, May 10, 2013 at 9:04 AM, MigMit <migue...@yandex.ru> wrote:

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:

Right, that is an alternative solution,  but phantom types are a relatively simple and well understood way of enforcing this kind of property in the type system without incurring run-time costs.   My inotify binding is intended to be as thin as possible,  and given my proposed interface,   you could implement your interface in terms of mine,  making the phantom types disappear using the restricted existentials already available in GHC,   and such a wrapper should be just as efficient as if you had implemented your interface directly.

Best,

Leon

[Alexander Solla]

I'm not sure if it would work for your case, but have you considered using DataKinds instead of phantom types?  At least, it seems like it would be cheap to try out.

http://www.haskell.org/ghc/docs/7.4.2/html/users_guide/kind-polymorphism-and-promotion.html

[Leon Smith]

On Fri, May 10, 2013 at 5:49 PM, Alexander Solla <alex....@gmail.com> wrote:

I'm not sure if it would work for your case, but have you considered using DataKinds instead of phantom types?  At least, it seems like it would be cheap to try out.

http://www.haskell.org/ghc/docs/7.4.2/html/users_guide/kind-polymorphism-and-promotion.html

I do like DataKinds a lot,  and I did think about them a little bit with respect to this problem,  but a solution isn't obvious to me,  and perhaps more importantly I'd like to be able to support older versions of GHC,  probably back to 7.0 at least.

The issue is that every call to init needs to return a slightly different type,  and whether this is achieved via phantom types or datakinds,  it seems to me some form of existential typing is required.  As both Andres and MigMit pointed out,  you can sort of achieve this by using a continuation-like construction and higher-ranked types (is there a name for this transform?  I've seen it a number of times and it is pretty well known...),  but this enforces a dynamic extent on the descriptor whereas the original interface I proposed allows an indefinite extent.

Best,

Leon

[Alexander Solla]

I know what extensions (of predicates and the like) are, but what exactly does "dynamic" and "indefinite" mean in this context?

[Leon Smith]

A value has an indefinite extent if it's lifetime is independent of any block of code or related program structure,  think malloc/free or new/gc.  A value has a dynamic extent if is lifetime is statically determined relative to the dynamic execution of the program (e.g. a stack variable):  in this case the type system ensures that no references to the inotify descriptor can exist after the callback returns.  

Best,
Leon

[ol...@okmij.org]

But Haskell (and GHC) have existential types, and your prototype code
works with GHC after a couple of trivial changes:

> main = do
> W nd0 <- init

> wd0 <- addWatch nd0 "foo"

> wd1 <- addWatch nd0 "bar"

> W nd1 <- init

> 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

The only change is that you have to write
W nd <- init
and that's all. The type-checker won't let the user forget about the
W. The commented out lines do lead to type errors as desired.

Here is what W is

> data W where
> W :: Inotify a -> W
> init :: IO W
[trivial modification to init's code]

I must say though that I'd rather prefer Adres solution because his
init

> init :: (forall a. Inotify a -> IO b) -> IO b

ensures that Inotify does not leak, and so can be disposed of at the
end. So his init enforces the region discipline and could, after a
trivial modification to the code, automatically do a clean-up of
notify descriptors -- something you'd probably want to do.

[Roman Cheplyaka]

* ol...@okmij.org <ol...@okmij.org> [2013-05-11 05:26:55-0000]

> I must say though that I'd rather prefer Adres solution because his
> init
> > init :: (forall a. Inotify a -> IO b) -> IO b
>
> ensures that Inotify does not leak, and so can be disposed of at the
> end. So his init enforces the region discipline and could, after a
> trivial modification to the code, automatically do a clean-up of
> notify descriptors -- something you'd probably want to do.

Well, it is still possible to escape if one wants, using an existential
type:

data Escape = forall a . Escape (Inotify a) (Watch a)

main = do
Escape inotify watch <-
init $ \inotify -> do
watch <- addWatch inotify "foo"
return $ Escape inotify watch

rmWatch inotify watch

This is because here, unlike in the ST case, the monad itself (IO) is not tagged.

It's probably not easy to do this by accident, but I think "ensures" is
too strong a word here.

Roman

[ol...@okmij.org]

> > I must say though that I'd rather prefer Adres solution because his
> > init
> > > init :: (forall a. Inotify a -> IO b) -> IO b
> >
> > ensures that Inotify does not leak, and so can be disposed of at the
> > end. So his init enforces the region discipline and could, after a

> It's probably not easy to do this by accident, but I think "ensures" is
> too strong a word here.

Indeed. I should've been more precise and said that 'init' -- like
Exception.bracket or System.IO.withFile -- are a good step towards
ensuring the region discipline. One may wish that true regions were
used for this project (as they have been for similar ones, like
usb-safe).