Re: [Haskell-cafe] Type system trickery

Niklas Broberg wrote:

On Sun, Jun 21, 2009 at 9:24 PM, Andrew Coppin 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...