[Haskell-cafe] Re: An interesting monad: "Prompt"
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
you need to use coinduction. For more, see also
http://www.cs.nott.ac.uk/~gmh/bib.html#corecursion
Regards,
apfelmus
More information about the Haskell-Cafe
mailing list