David Menendez dave at zednenem.com
Sun Dec 14 02:50:28 EST 2008

```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,
>>
>>
>> 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?

someone might *want* a rank-3 signature for callCC. It involves a

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/>
```