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

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

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