apfelmus apfelmus at quantentunnel.de
Fri Jan 4 06:59:59 EST 2008

```Felipe Lessa wrote:
> Ryan Ingram 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

You probably mean

runPromptM id = id

> 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?

You want to deduce

runPromptM id (Prompt pa c) = Prompt pa c

from

runPromptM id (Prompt pa c) = Prompt pa (runPromptM id . c)

by somehow assuming that  runPromptM id = id  at least when applied to
c . If it were a problem about lists like

foldr (:) [] = id

you could use  mathematical induction . You can do the same here, but