Re: [Haskell-cafe] 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). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A use case for *real* existential types
* o...@okmij.org [2013-05-11 05:26:55-] > 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 wrote: > > > > On Fri, May 10, 2013 at 3:31 PM, Leon Smith wrote: > >> On Fri, May 10, 2013 at 5:49 PM, Alexander Solla 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. >> > > 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A use case for *real* existential types
On Fri, May 10, 2013 at 3:31 PM, Leon Smith wrote: > On Fri, May 10, 2013 at 5:49 PM, Alexander Solla 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. > 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A use case for *real* existential types
On Fri, May 10, 2013 at 5:49 PM, Alexander Solla 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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. http://www.haskell.org/ghc/docs/7.4.2/html/users_guide/kind-polymorphism-and-promotion.html On Fri, May 10, 2013 at 12:52 PM, Leon Smith wrote: > On Fri, May 10, 2013 at 9:04 AM, MigMit 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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A use case for *real* existential types
On Fri, May 10, 2013 at 9:04 AM, MigMit 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A use case for *real* existential types
On Fri, May 10, 2013 at 9:00 AM, Andres Löh 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 n
Re: [Haskell-cafe] 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] 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. inotify.hs Description: Binary data ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
