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

[apfelmus]

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 
you need to use coinduction. For more, see also

   http://www.cs.nott.ac.uk/~gmh/bib.html#corecursion


Regards,
apfelmus