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

oleg at okmij.org oleg at okmij.org
Sat May 11 07:26:55 CEST 2013


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.





More information about the Haskell-Cafe mailing list