[Agda] IO in Agda.

[Peter G. Hancock]

>>>>> Marcin Benke wrote (on Thu, 09 Dec 2004 at 13:29):

    > Peter G. Hancock wrote:
    >> 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.
    > On the practical side, we have an experimantal version of class system,
    > which means we may have monads similar to ones in Haskell, and
    > Catarina is working on do-notation.

Is the class system something like Haskell's?  Or can it be understood
by human beings? :-) 

It is nice to have monadic notation, but I think more subtle matters
are important with IO programs.  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.

One point is that in dependent type theory the IO monad is really
at the level of predicates (set-valued-functions), not of sets. 

If I understand what Pierre is doing, there is a state space (in terms
of which the semantics of the operations is explained), and the key
things are transformers of state-predicates.  

To recover the Haskell IO system, the set of states would have to be 
a singleton. 

Instead, one key thing is a relation Prog(s,U) which is the set of 
programs which can be run in state s that exit only in a state 
satisfying predicate U.  Without the parameters, one can define
IO(a) = (a -> Prog)->Prog.  But with the parameters, things are
more complicated.  

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.

Maybe Prog and coProg are a better foundation than an IO monad on Set? 

Peter Hancock