[Agda] Future of Agda?

[Peter G. Hancock]

>>>>> Pierre Hyvernat wrote (on Mon, 13 Dec 2004 at 15:08):

    >   * getting a smaller, better Agda (with a source code as simple
    >   as we can get it)

That is what I would like.  Of course it is much more difficult than
feature-rich agda.

    > My view is thus that we should have a "core Agda" as small and nice as
    > possible. This would contain more or less what Agda contains now.  (I
    > guess this is what Agda-light is aiming at.)

I suggest that Agda which disallows *any* recursion is the basic level of
Agda one wants.  (But not of course all.) 

    > Together with that, we should try to design a good pluggin mechanism and
    > an emacs interface (pretty much similar to what we use now) and good
    > documentation.

I entirely agree.  These are both interface issues.

* between checker and front end.  This can be perhaps be looked at in
 the light of epigram, proof-general, alfa and such things.  

* between someone's termination checker and the trusted core. 

But I want to stress the importance of the IO interface.  I have to
admit that although I broadly agree with Pierre that one wants to type
both terminating and looping programs, I don't really see exactly how
it should be expressed and made to work.  I was hoping to initiate
some suggestions.  What are these abstract states and what role do
they play?

Plenty when you are specifying IO primitives, or writing programs that
use them (I contend); but none at run-time.  The states have done their job
by the time the program runs. 

I don't think one should focus just on stream IO here (putchar and getchar);
it is a very special case.  One might also try to imagine how the less exotic
part of lazyml's IO, or Fudget's might work in Agda.  

There is also the side issue of somehow coercing values to IO programs, as with
the haskell show mechanism.  I expect that here "classes" come in. 
I'd be really interested in what kind of class system is proposed.

\begin{joke} 
Is it going to be a playground for prolog programmers and
people with a sick sense of humour, such as the Haskell class
system has become?  
\end{joke}

Peter