On Jan 4, 2008 9:59 AM, apfelmus <[EMAIL PROTECTED]> wrote: > Felipe Lessa wrote: > > How can we prove that (runPromptM prompt === id)? I was trying to go with > > You probably mean > > runPromptM id = id >
Actually, I meant an specialization of 'runPromptM prompt': runPromptM id :: (Monad p) => Prompt p r -> p r runPromptM prompt :: (MonadPrompt p m) => Prompt p r -> m r runPromptM (prompt :: p a -> Prompt p a) :: Prompt p r -> Prompt p r [snip] > 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 > Thanks for the tip! So I can define > approx :: Integer -> Prompt p r -> Prompt p r > approx (n+1) (PromptDone r) = PromptDone r > approx (n+1) (Prompt p c) = Prompt p (approx n . c) > > runId :: Prompt p r -> Prompt p r > runId = runPromptM prompt and try to prove that ∀n. approx n (id x) == approx n (runId x) We can see trivially that approx n (id (PromptDone r)) == approx n (runId (PromptDone r)) For the case that x is (Prompt p c), we'll prove using induction. The base case n = 0 is trivially proven as ∀x. approx 0 x == ⊥. For the indutive case, approx (m+1) (runId (Prompt p c)) -- definition of runId = approx (m+1) (runPromptM prompt (Prompt p c)) -- definition of runPromptM for the Prompt case = approx (m+1) (prompt p >>= runPromptM prompt . c) -- definition of prompt in the Prompt instance = approx (m+1) (Prompt p return >>= runPromptM prompt . c) -- definition of (>>=) in the Prompt instance = approx (m+1) (Prompt p ((>>= runPromptM prompt . c) . return)) -- monad law '(return x >>= f) == f x' = approx (m+1) (Prompt p (runPromptM prompt . c)) -- definition of approx = Prompt p (approx m . runPromptM prompt . c) -- definition of runId = Prompt p (approx m . runId . c) -- definition of (.) twice = Prompt p (\x -> approx m (runId (c x))) -- induction hypothesis = Prompt p (\x -> approx m (id (c x)) -- definition of (.) twice = Prompt p (approx m . id . c) -- definition of approx = approx (m+1) (Prompt p (id . c)) -- law 'id . f == f' = approx (m+1) (Prompt p c) -- law 'x == id x' = approx (m+1) (id (Prompt p c)) Which was to be proven. ∎ I think I didn't commit any mistake above =). Thanks again for help, -- Felipe.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe