On Sat, Dec 13, 2008 at 6:00 PM, Andrew Coppin <andrewcoppin@btinternet.com> wrote:
David Menendez wrote:
On Thu, Dec 11, 2008 at 1:48 PM, Andrew Coppin <andrewcoppin@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@zednenem.com> <http://www.eyrie.org/~zednenem/>