[Haskell-cafe] Can we come out of a monad?

[John Meacham]

On Sat, Jul 31, 2010 at 01:49:43AM +0400, Alexey Khudyakov wrote:
> No I think here we breaking out from _arbitrary_ monad. If monadic
> function works for every monad then it must work for identity monad
> too. Here is simplest form of purify function:
> 
> > purify2 :: (forall m . Monad m => m a) -> a
> > purify2 m = runIdentity m
> 
> This proves interesting fact. Value could be removed from monad if no
> constrain is put on the type of monad. Moreover it Monad in this
> example could be replaced with Functor or other type class

This becomes much more clear when you float the quantifier to the top
level: 

> purify2 :: (forall m . Monad m => m a) -> a

since the quantifier is in an argument position, to float it out, we
need to flip it, it goes from universal to existential quantification.
so we get the equivalent type:

> purify2' :: exists m . Monad m => (m a -> a)

which you can read as "there exists some monad for which you can pull
out its value". The implementation is just the witness that proves that
Identity is one such monad, satisfying the existential quantification.

        John

-- 
John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/