[Haskell-cafe] Type system trickery

[David Menendez]

On Sun, Jun 21, 2009 at 4:00 PM, Andrew
Coppin<andrewcoppin at btinternet.com> wrote:
> Niklas Broberg wrote:
>>
>> On Sun, Jun 21, 2009 at 9:24 PM, Andrew
>> Coppin<andrewcoppin at 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 <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>