[Haskell-cafe] Type system trickery

[Andrew Coppin]

Niklas Broberg wrote:
> On Sun, Jun 21, 2009 at 9:24 PM, Andrew
> Coppin<andrewcoppin at btinternet.com> wrote:
>   
>>  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
>   

...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.)

A slight complication is that Foobar refers to a second type which 
exhibits a similar behaviour - but presumably I can utilise the same 
solution there also...