[Agda] IO, semi-closed handles, and problems with extensional equality

[Peter Hancock]

There are monads (and comonads) "all over the place" in what Anton describes.  The notion of monad, as Moggi realised, provides us with some basic kit with which to model sequencing and termination of effectful programs.  Nowadays, I think many people have realised that when we have said everything we can or need to say about sequencing and termination, we have said nothing at all about what an effect is, how effects arise when an effectful program runs, or how we might prove that an effectful program, when run, behaves in accordance with its specification.  

To me, with a dependently typed language, we have the opportunity to really address the question of specifying effectful programs, with full precision.  To take this opportunity, we may have to be ready to re-think the ideas that we bring to this area from languages such as haskell. (Or Clean, for that matter.)  My own thoughts, with Anton and with other people, have taken me back decades before Moggi, to the foundations of imperative programming, to predicate transformers, and the tradition started by Hoare, Dijkstra, and particularly the refinement calculus of Carroll Morgan, Back and von Wright.

This thread isn't a suitable place in which to cram everything that needs to be said on IO in Agda (even if I knew what it was).  Let me just say two tiny things -- one about monads, and one about interfaces.

1. Monads.  As everyone knows, a monad is an endofunctor on a
   category, with some extra structure (the multiplication and the
   unit).  Coming from haskell, we're in danger of forgetting that the category
   need not be the category of sets.  It may, for example
   be the functor category (S -> Set), where S is a statespace
   (a discrete category, at least in the first place)
   in terms of which we specify the operations of an interface. 
   The objects of this category are predicates, and the morphisms
   are predicate transformers.  In this category we have the usual
   notion of free monad over a functor (F^* = mu X. Y + F X) and 
   some other monads (nu X. Y + F X), comonads, and other categorical 
   gadgetry (comonads, adjunctions, algebras, etc etc) that's 
   prov so worthwhile in the context of haskell, and is just
   as valuable in the dependently typed case as in haskell-ville.
   But the categories may be a bit different.

2. Interfaces.  Having worked for a long time in systems programming, 
   I'm puzzled by the way people seemingly plant themselves
   firmly on the "program" side of an interface, and seldom on the
   "environment" side.  Most of the code I have ever written has in fact
   been a layer, or component, that sits between *two* (at least) 
   interfaces.  With respect to one of these interfaces, the code 
   plays the role of a client; with respect to the other, it plays the
   role of a server.  The first interface looks monadic; in contrast,
   the second is comonadic.  The program component itself implements
   a *simulation* of the "higher" interface by the "lower" (as was 
   first realised I think by Hoare).  

What I really want to say is *not* that the Agda community should swallow my or Anton's ideas in figuring out how effects should look or work in Agda.  I want to plead with you to realise that you have an opportunity to *enrich* and *extend* and *go beyond* things like the IO monad of haskell. To me the prize to be gained is a rigorously founded way of writing *specifications* (in a language, in which after all we can write down any proposition of constructive mathematics), and a way to developing programs that not only "do things", but actually do what they are supposed to.  The central thing is specification. 

Hank