[Haskell-cafe] Type system trickery

[Niklas Broberg]

On Sun, Jun 21, 2009 at 9:24 PM, Andrew
Coppin<andrewcoppin at btinternet.com> wrote:
> I have a datatype with about a dozen constructors. I'd like to find a way to
> use the type system to prevent one of the constructors from being used in
> certain places. But I can't think of a way to do that.
>
>  data Foobar =
>   Foo Foobar |
>   Bar Foobar |
>   Zoo Foobar
>
> I want the type system to track whether or not Zoo has been used in a
> specific value. Sure, you can check for it at runtime, but I'd be happier if
> the type system can guarantee its absence when required.

That's what GADTs are for:

data Flag = HasZoo | NoZoo

data Foobar a where
  Foo :: Foobar a -> Foobar a
  Bar :: Foobar a -> Foobar a
  Zoo :: Foobar a -> Foobar HasZoo

f :: Foobar NoZoo -> Int
f foobar = ... -- foobar cannot be Zoo here

Cheers,

/Niklas