[Agda] Good old times

[Pierre Hyvernat]

Some additional comments, and call for reactions



>>   what about a minimal Agda2,
> It would be nice to have a well-understood core theory, which full
> Agda could be compiled into.
>
I remember discussions about that at the Agda meeting last May. I wasn't
convinced this was possible, or even desirable.

Seeing the evolution of Agda, I am now sure this is impossible. (The
core would need coinduction for example, and I'm not sure this is a good
idea at the moment...)



What would be possible is to have a minimal logical framework (dependent
products, dependent records, inductive types, Set and Type). I'm not
even sure I'd want inductive families in there...

I am thinking, something along the lines of Thierry's first prototypes,
with: decent error reporting, minimal standard library, small Emacs
mode.
It could be done in less than 2000 loc. (Random guess.)


Once this thing is agreed upon (trouble ahead) and working, it can be
"frozen". (Just like haskell98.)




The full blown Agda would use the same theory at the core but with all
the additional features (coinduction, inductive families, sized types,
testing, exceptions, impredicative universes, documentation generator,
web browser, ...)

The idea to translate everything to this minimal core seems to
contradict the idea of having something even moderately optimized.




About the dependencies, what concerns me is to see Agda depending on
such things as "xhtml-3000.2.0.1" and others.  I mean, part of Agda is
about the foundation of mathematics. It is not just another programming
language...




> Preferably with a type-checker written in Agda itself (using some form
> of stratification to avoid circularity).  However, this is a separate
> issue.
>
I'd say we wait a little before trying to take over the world... :)


Pierre
-- 
Computer Science is not about computers, any more than
astronomy is about telescopes.
    -- Edsger Wybe Dijkstra