On Sun, Jun 21, 2009 at 4:00 PM, Andrew
Coppin<andrewcop...@btinternet.com> wrote:
> Niklas Broberg wrote:
>>
>> On Sun, Jun 21, 2009 at 9:24 PM, Andrew
>> Coppin<andrewcop...@btinternet.com> 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 <d...@zednenem.com>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
