[Haskell-cafe] Type system trickery

[Niklas Broberg]

>> That's what GADTs are for:
>>
>> data Flag = HasZoo | NoZoo

Eh, I wrote this a bit fast obviously (no dependent types here).

Like Daniel Fischer wrote, these should rather be separate data types, i.e.

data HasZoo
data NoZoo

The rest is still correct though.

>> data Foobar a where
>>  Foo :: Foobar a -> Foobar a
>>  Bar :: Foobar a -> Foobar a
>>  Zoo :: Foobar a -> Foobar HasZoo
>
> ...so I use "Foobar x" to mean any kind of value, "Foobar NoZoo" for a value
> that definitely doesn't contain Zoo, and "Foobar HasZoo" for... one that
> definitely does? Or maybe does? (Not that I care about this, but for
> completeness I'd like to know.)

Yep, you are correct. Actually, you don't have to use NoZoo, you could
use e.g. Foobar () or Foobar (Maybe Bool) if you like. Anything that
isn't HasZoo.

Cheers,

/Niklas