[Haskell-cafe] Re: An interesting monad: "Prompt"

[Felipe Lessa]

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.