On Nov 18, 2007 10:22 PM, Ryan Ingram <[EMAIL PROTECTED]> 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 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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
