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/