[Agda] interactive mode

[Conor McBride]

Hi folks

I feel slightly wistful reading this thread...
never mind.

On 9 Jun 2008, at 11:59, Andres Loeh wrote:

> Hi Thorsten.
>
>> have you actually tried the emacs mode? It is becoming the  
>> standard way to
>> develop Agda programs, and it is quite usable these days & I  
>> suspect that
>> it is more productive then using the interactive mode.
>
> Yes, I have, and I agree that it is quite good. Anyway, even though I
> had everything set up for emacs, I found myself switching back to vim
> and --interactive after a while ...

There's a tension between the free choice of
editing technology and the non-trivial
interactions which are central to the
dependently typed programming process. For a
change, we do write programs with computers:
we don't just type them in!


>
>> I agree that ideally the programming language shouldn't dictate the
>> development tools. Agda is doing better than Epigram, it allows  
>> you to use
>> a batch mode and it's emacs interface is more flexible.  
>> Dependently typed
>> languages redefine this question, because one could argue that the  
>> ability
>> to batch "compile" your programs is not enough you also want a low- 
>> tech
>> interface to interactive program development/
>
> I agree here as well. I certainly don't want to bash the emacs  
> mode, and
> I discourage its further development. I just think that it would be  
> nice
> if it wouldn't be the only choice for interactive development ...

It seems to me that we might learn from version
control systems, which seem to cooperate with
many editors. We could perhaps set things up so
that Agda acted as a kind of co-cauthor, sometimes
grumpy, sometimes helpful, responding to patches
pushed with patches of its (her?) own. It's
probably useful in practice to maintain a "live"
Agda in sync with a "repo" you're actively
fiddling with, much as people editing the same
document in the same room often react to each
other quite effectively as patches fly around.

Would it be so tricky to mediate the current
interactive technology (requests for information,
or other forms of automated help, responses
rude or otherwise) entirely within the text of
source files, so that Agda could be presented
entirely as a boring old stdin->stdout
transducer? Might that be one way to provide
lowest common denominator support for multiple
editors, whilst retaining the "conversational"
approach?

Cheers

Conor