Re: [Haskell-cafe] Type system trickery

On Sun, Jun 21, 2009 at 4:00 PM, Andrew Coppin wrote:

Niklas Broberg wrote:

...

On Sun, Jun 21, 2009 at 9:24 PM, Andrew Coppin wrote:

...

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:

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

If you don't need code that's polymorphic between Foobar HasZoo and Foobar NoZoo, you could just newtype Foobar and only export smart constructors. module NoZoo (NoZoo, noZoo, mkNZ, mkNZ', unNZ) where newtype NoZoo = NZ Foobar noZoo :: Foobar -> Bool noZoo = ... mkNZ :: Foobar -> NoZoo mkNZ = NZ . assert "Zoo" . noZoo mkNZ' :: Foobar -> Maybe NoZoo mkNZ' x | noZoo x = Just x | otherwise = Nothing unNZ :: NoZoo -> Foobar unNZ (NZ x) = x Assuming noZoo is written correctly, this is enough to guarantee that unNZ never produces a value of Foobar containing Zoo. Oleg Kiselyov and Chung-chieh Shan have written about this. Try http://okmij.org/ftp/Computation/lightweight-dependent-typing.html or search for "lightweight static capabilities". -- Dave Menendez http://www.eyrie.org/~zednenem/