[Haskell-cafe] Re: An interesting monad: "Prompt"
Felipe Lessa
felipe.lessa at gmail.com
Fri Jan 4 08:46:13 EST 2008
On Jan 4, 2008 9:59 AM, apfelmus <apfelmus at quantentunnel.de> 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.
More information about the Haskell-Cafe
mailing list