[Haskell-cafe] Type system trickery

[Daniel Fischer]

Am Sonntag 21 Juni 2009 21:24:24 schrieb Andrew Coppin:
> 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.
>
> I tried this:
>
>   data Zoo x =
>     Zoo x |
>     NoZoo x
>
>   data GeneralFoobar f =
>     Foo f |
>     Bar f
>
>   type Foobar = GeneralFoobar Foobar
>   type FoobarZ = GeneralFoobar (Zoo FoobarZ)
>
> but the type checker seems to not like it. (Plus I now have to wade
> through miles of NoZoo wrappers everywhere.)
>
> The other alternative is to just duplicate the entire data declaration,
> sans the Zoo constructor... but I'd obviously prefer not to have to do
> that. (E.g., if I ever need to alter the declaration, I now have two
> copies to keep in sync.)
>
> Suggestions?

GADTs?

data Okay
data HasZoo
data Aye
data Nay

class IsOkay a b | a -> b where

instance IsOkay Okay Aye where

instance IsOkay HasZoo Nay where

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

use :: (IsOkay a Aye) => Foobar a -> whatever