Re: [Haskell-cafe] A curios monad

On Sat, Dec 13, 2008 at 6:00 PM, Andrew Coppin wrote:

David Menendez wrote:

...

On Thu, Dec 11, 2008 at 1:48 PM, Andrew Coppin 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 http://www.eyrie.org/~zednenem/