[Haskell-cafe] An interesting monad: "Prompt"

[Felipe Lessa]

On Nov 18, 2007 10:22 PM, Ryan Ingram <ryani.spam at gmail.com> wrote:
[snip]
> > data Prompt (p :: * -> *) :: (* -> *) where
> >     PromptDone :: result -> Prompt p result
> >     -- a is the type needed to continue the computation
> >     Prompt :: p a -> (a -> Prompt p result) -> Prompt p result
[snip]
> > runPromptM :: Monad m => (forall a. p a -> m a) -> Prompt p r -> m r
> > runPromptM _ (PromptDone r) = return r
> > runPromptM f (Prompt pa c)  = f pa >>= runPromptM f . c
[snip]

How can we prove that (runPromptM prompt === id)? I was trying to go with

runPromptM prompt (PromptDone r)
 = return r
 = PromptDone r

runPromptM prompt (Prompt pa c)
 = prompt pa >>= runPromptM prompt . c
 = Prompt pa return >>= runPromptM prompt . c
 = Prompt pa ((>>= (runPromptM prompt . c) . return)
 = Prompt pa (runPromptM prompt . c)

... and I got stuck here. It "seems obvious" that we can strip out the
'runPromptM prompt' down there to finish the proof, but that doesn't
sound very nice, as I'd need to suppose what I'm trying to prove. Am I
missing something here?

Thank you,

-- 
Felipe.