[Haskell-cafe] Re: MonadPrompt + Gtk2Hs = ?

[apfelmus]

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