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.
* oleg@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 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
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).
participants (2)
-
oleg＠okmij.org -
Roman Cheplyaka