On Nov 18, 2007 10:22 PM, Ryan Ingram
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.