An interesting monad: "Prompt"

[Felipe Lessa]

On Nov 18, 2007 10:22 PM, Ryan Ingram <ryani.spam@...> 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@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Heinrich Apfelmus]

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@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Felipe Lessa]

On Jan 4, 2008 9:59 AM, apfelmus <apfelmus@...> 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@...
http://www.haskell.org/mailman/listinfo/haskell-cafe