[Haskell-cafe] A curios monad

[David Menendez]

On Sat, Dec 13, 2008 at 6:00 PM, Andrew Coppin
<andrewcoppin at btinternet.com> wrote:
> David Menendez wrote:
>>
>> On Thu, Dec 11, 2008 at 1:48 PM, Andrew Coppin
>> <andrewcoppin at btinternet.com> wrote:
>>
>>>
>>> BTW, does anybody know how rank-N types are different from existential
>>> types?
>>>
>>
>> You mean the Haskell extensions?
>>
>> ExistentialQuantification lets you define types such as,
>>
>>    data SomeNum = forall a. Num a => SomeNum a
>>
>> RankNTypes lets you nest foralls arbitrarily deep in type signatures,
>>
>>    callCC :: ((forall b. a -> m b) -> m a) -> m a   -- this is rank-3
>>
>> RankNTypes implies ExistentialQuantification (among others).
>>
>
> So how is
>
>  foo :: ((forall b. a -> m b) -> m a) -> m a
>
> different from
>
>  bar :: forall b. ((a -> m b) -> m a) -> m a
>
> then?

Daniel Fischer already gave the short answer, I'll try explaining why
someone might *want* a rank-3 signature for callCC. It involves a
continuation monad, but hopefully nothing headache-inducing.

The type for callCC in Control.Monad.Cont.Class is,

callCC :: forall m a b. (MonadCont m) => ((a -> m b) -> m b) -> m b

You can use callCC to do very complicated things, but you can also use
it as a simple short-cut escape, like the way "return" works in C.

foo = callCC (\exit -> do
    ...
    x <- if something
        then return 'a'
        else exit False
    ...
    return True)

The type of exit is Bool -> m Char, which is fine in this example, but
it means that we can only use exit to escape from computations that
are producing characters. For example, we cannot write,

bar = callCC (\exit -> do
    ...
    x <- if something then return 'a' else exit False
    y <- if something then return 42 else exit False
    ...
    return True)

Because exit would need to have the type Bool -> m Char the first time
and Bool -> m Int the second time. But, if callCC had a rank-3 type,

callCC :: forall m a. (MonadCont m) => ((forall b. a -> m b) -> m a) -> m a

then exit would have the type "forall b. Bool -> m b", and bar would
compile just fine.

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>