[Agda] Interactive programs in Agda

[Anton Setzer]

Peter Hancock wrote:
> 
> By the way, thanks very much for the library and slides.
> 
>>
>> and is linked from
>> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Libraries
>>
> Looking at the slides for your AIM talk linked from here,
> I think you define
> 
>    IO C R A to be  nu X.  A + (C <| R) X
> 
> to use container notation.   This is monadic in A, but I think the
> proof is a little tricky.


I think the proof wouldn't be too complicated  by guarded recursion
which is equivalent (in its simplest form) or follows (in  some
more advanced form) from the elimination rules for coalgebras.
But its a bit of work, I haven't done it yet. Equalities
would hold only w.r.t. bisimulation, I assume.

> 
> You give on slide 8 a "definition" of >>= which would work
> fine if the IO C R A were mu X. A + (C <| R) X.
> Can the definition really be justified from the universal property of
> final coalgebras?

_>>=_  is defined by guarded recursion in the first argument which
follows from the introduction rules.
More precisely it is as follows:

The standard introduction rules for coalgebras give you

     B : Set       f : B -> ((c : C) x (R c -> B))  +   A
   ----------------------------------------------------
                 intro (B ,f ) : B -> IO A

and have
    elim : IO A -> (( c: C) x (R c -> IO A))  + A
    elim ( intro B f) = case f b of
                   inl (<c,g>) -> inl (c,\r -> intro B f (g r))
                   inr a       -> a

>From this we can derive (up to bisimulation) an advanced introduction
principle, which allows us to escape at any time:

      B : Set      f : B -> ((c : C) x (R c -> (A + IO A)) + A
     -------------------------------------------------------------
                    intro'  B f : B -> IO A

elim (intro' B f) = case f b of
          inl (<c,g>) -> inl   (c, \ r ->    [(intro B f),id](g r))
          inr a       -> a

So if f0 := intro' B f
     f b = inl (<c,g>)
        then elim (f b) computes to   do c h
            where h r = f0 b'    if g r = inl b'   (recursion)
            and   h r = q       if g r = inr q     (jumping out of the

                                                    recursion)
  if f b = inr a
        then (intro B f b) computes to return a


In this example we take the second argument q of _>>=_ as
parameter and let B = IO A for  which we take the  first argument
So we need to defin
     f:  IO A -> ((c : C ) x (R c -> IO A + IO A)) + A
     f p = case elim(p) of
               do c p' ->   inl (<c,\ r -> inl (p' r)>)
               return a ->  case (q a) of
                               return a' -> inr a
                               do c q    -> inr (<c, \ r -> inr (q r)>)



> 
> I wonder if people in the future will say "It was 2009 when
> Anton Setzer dragged a window across his monitor using a
> his mouse and a constructive proof". The importance of this
> moment in history may overshadow the invention of the wheel.
> 
> Peter


Anton

-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------