Felipe Lessa wrote:
apfelmus wrote:
The type of contPromptM is even more general than that:
casePromptOf' :: (r -> f b) -> (forall a,b. p a -> (a -> f b) -> f b) -> Prompt p r -> f b casePromptOf' done cont (PromptDone r) = done r casePromptOf' done cont (Prompt p c ) = cont p (casePromptOf' done cont . c)
(I guess the forall b inside 'cont' is a typo?)
No, it's intentional and not less general than
casePromptOf :: (r -> b) -> (forall a. p a -> (a -> b) -> b) -> Prompt p r -> b casePromptOf done cont (PromptDone r) = done r casePromptOf done cont (Prompt p c ) = cont p (casePromptOf done cont . c)
since we can use data Const c b = Const { unConst :: c } and set f = (Const b) yielding casePromptOf :: forall p,c. (r -> c) -> (forall a. p a -> (a -> c) -> c) -> Prompt p r -> c casePromptOf return bind = unConst . casePromptOf' (Const . return) bind' where bind' :: forall a,b. p a -> (a -> Const c b) -> Const c b bind' p c = Const $ bind p (unConst . c) In other words, casePromptOf can be defined with casePromptOf' and a clever choice of f .
And, just for the record,
runPromptAgain :: Monad m => (forall a. p a -> m a) -> Prompt p r -> m r runPromptAgain f = casePromptOf return ((>>=) . f)
I thought that casePromptOf would not be general enough to write this very definition runPromptAgain' f = casePromptOf' return ((>>=) . f) that's why I used a type constructor f b instead, with f = m the monad in mind. The difference is basically that the (>>=) in runPromptAgain' is expected to be polymorphic (>>=) :: forall b. m a -> (a -> m b) -> m b whereas the (>>=) in runPromptAgain is specialized to the final type m r of runPromptAgain , i.e. (>>=) :: m a -> (a -> m r) -> m r Unfortunately, I failed to realize that casePromptOf is in turn not less general than casePromptOf' rendering my approach pretty useless :) I mean, if the second argument in casePromptOf' :: (r -> f c) -> (forall a,b. p a -> (a -> f b) -> f b) -> Prompt p r -> f c is polymorphic, we can certainly plug it into casePromptOf :: (r -> f c) -> (forall a. p a -> (a -> f c) -> f c) -> Prompt p r -> f c and thus define casePromptOf' in terms of casePromptOf : casePromptOf' return bind = casePromptOf return bind The above equivalence of a type constructor f and a simple type c in certain cases applies to the continuation monad, too. I mean that ContT r m a is equivalent to Cont (m r) a and even ContT' m a is equivalent to forall r. Cont (m r) a for the more type safe version data ContT' m a = ContT' (forall r. (a -> m r) -> m r) So, it's pretty clear that ContT isn't really a monad transformer since m doesn't need to be a monad at all. Put differently, the Control.Monad.Cont module needs some cleanup since type synonyms type ContT r m a = Cont (m r) a type ContT' m a = forall r. Cont (m r) a (or newtypes for type classery) are enough. Regards, apfelmus