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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
