Leon Smith | 10 May 12:17 2013
Picon

A use case for *real* existential types

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.
Attachment (inotify.hs): application/octet-stream, 1750 bytes
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Andres Löh | 10 May 15:00 2013

Re: A use case for *real* existential types

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
Leon Smith | 10 May 21:36 2013
Picon

Re: A use case for *real* existential types

On Fri, May 10, 2013 at 9:00 AM, Andres Löh <andres <at> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
MigMit | 10 May 15:04 2013
Picon

Re: A use case for *real* existential types

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
Leon Smith | 10 May 21:52 2013
Picon

Re: A use case for *real* existential types

On Fri, May 10, 2013 at 9:04 AM, MigMit <miguelimo38 <at> 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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Alexander Solla | 10 May 23:49 2013
Picon

Re: A use case for *real* existential types

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.



On Fri, May 10, 2013 at 12:52 PM, Leon Smith <leon.p.smith <at> gmail.com> wrote:
On Fri, May 10, 2013 at 9:04 AM, MigMit <miguelimo38 <at> 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


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Leon Smith | 11 May 00:31 2013
Picon

Re: A use case for *real* existential types

On Fri, May 10, 2013 at 5:49 PM, Alexander Solla <alex.solla <at> 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.


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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Alexander Solla | 11 May 00:52 2013
Picon

Re: A use case for *real* existential types




On Fri, May 10, 2013 at 3:31 PM, Leon Smith <leon.p.smith <at> gmail.com> wrote:
On Fri, May 10, 2013 at 5:49 PM, Alexander Solla <alex.solla <at> 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.


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.

I know what extensions (of predicates and the like) are, but what exactly does "dynamic" and "indefinite" mean in this context?
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Leon Smith | 11 May 01:02 2013
Picon

Re: A use case for *real* existential types

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


On Fri, May 10, 2013 at 6:52 PM, Alexander Solla <alex.solla <at> gmail.com> wrote:



On Fri, May 10, 2013 at 3:31 PM, Leon Smith <leon.p.smith <at> gmail.com> wrote:
On Fri, May 10, 2013 at 5:49 PM, Alexander Solla <alex.solla <at> 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.


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.

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
oleg | 11 May 07:26 2013

A use case for *real* existential types


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 | 17 May 01:12 2013

Re: A use case for *real* existential types

* oleg <at> okmij.org <oleg <at> 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
oleg | 18 May 09:06 2013

Re: A use case for *real* existential types


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

Gmane