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