[Agda] IO in Agda.

[Pierre Hyvernat]

> > > Has there been any discussion of whether and how to represent an
> > > IO interface in Agda? Is this even on the radar?
> > >
> > Definitely.  Pierre Hyvernat is working on the theoretical side.
>
Well, both Peter Hancock, Anton Setzer and myself are (have been)
working on the theoretical side...



> It is nice to have monadic notation, but I think more subtle matters
> are important with IO programs.
>
Agreed.


>  One needs to decide how to use the type system to identify runnable
>  programs.  My opinion is that just taking the Haskell IO monad as a
>  monad on sets would be wrong.
>
I wouldn't say "wrong", but it certainly wouldn't be very exciting.
Dependent types would then appear only inside an IO program.

(I don't think the canonical examples like being able to type the
"printf" command are really interesting from a practical point of view.)




> One point is that in dependent type theory the IO monad is really at
> the level of predicates (set-valued-functions), not of sets.
>
Exactly, what Anton Setzer and Peter Hancock did some years ago is
precisely to define a "higher order" monad. I'll paraphrase what you've
written:

Compare

    A : Set                 (return values)
----------------
   IO(A) : Set              (IO programs which return a value in A)


to

S is a given set of "states"

       A : S -> Set         (A(s) : possible return values in state s)
-------------------------
      IO(A) : S -> Set

where p : IO A s means that p is an IO programs starting from state s
and returning values in A(final_state).



The first is haskell's IO monad, the second is the "higher order" monad
which one may want in dependent type theory.



Some problems are:

what is the set of states?

what is a good notation to write such programs?
(In my experience with those, the do notation is not very useful.)




The analogy Set=Prop allows for the following, more adequate reading:
  if A : S->Set is a subset of S
  p : IO(U,s)  is a program from starting state s which will terminate in
               a state in A


> In Pierre's analysis there is another relation coProg(s,U) that plays
> a similar role: the elements of coProg(s,U) are event-driven programs
> in a certain sense.
>
I just wrote IO(U,s) instead of Prog(s,U); but the key thing is exactly
that:
  p : IO(U,s)  means that p is a _terminating_ program starting in s
               terminating in U
  p : coIO(V,s) means that p is a _non-terminating_ program starting in s
                which always stays in V

Those seem to be the two main kinds of programs one is asked to write.

(writing non-terminating IO programs is _very important_: just to name
one of interest to us, "emacsagda" is of this kind...)



Pierre Hyvernat
--