FeatureRequests

Note: this page is somewhat stale.

Recent feature requests are documented on the bug tracker.

Language

• The operator precedences should not be required to form a total order, but rather a DAG.
• Proper pattern matching for records.
• DONE: Convenient record update syntax.
• Class system.
• A good story for how to "tackle the awkward squad".
• Injectivity test to boost constraint solving
• Make the module system a bit more flexible.
• DONE: Universe polymorphism.
• Haskell/Coq style type classes.

Implementation

• Print Reconstructed Terms
• Allow main() to return arbitrary values and print them automatically on exit.
• Better error messages.
• Reduced memory consumption.
• DONE: A nice interface between user interfaces and the backend should be designed and implemented. (This has been discussed on the mailing list.) Then the Emacs UI can be reconstructed on top of this new interface.
• It would be nice if one did not have to reload the file after every case-split, or to get highlighting after "give", for instance.
• It would be nice if Agda kept track of exactly which unsafe features have been used:

   $ agda --list-unsafe OK.agda
   $ agda --list-unsafe Dubious.agda
   Postulates used:
     ClassicalLogic.excluded-middle
   Does not termination check:
     Dubious.Internal.f
     Library.g
   Positivity checker turned off in:
     Dubious

Tools

• People complained when support was dropped for agda --interactive. James Chapman suggested that it would be nice to have a stand-alone interpreter (as opposed to a line-based editor). It should be possible to implement such an interpreter using the UI-backend interface suggested above. Note: It would be nice if one had the choice to run FFI code in such an interpreter.
• It might be nice to take agda --html further, constructing some sort of "AgdaDoc" tool. However, since the actual source code often matters, and not just the type signatures, one would have to think a bit first, and perhaps use some ideas from Coq or other systems.

Libraries

• The IO library is currently very small. It needs to be extended. We should also make use of strong types to improve the IO interface. This can be made in separate libraries, on top of a more low-level one which just uses the FFI to import Haskell functionality.
• Nice implementations of sets, maps, graphs etc. Here we have a problem: Implementation details should preferably be hidden (made abstract), but it is often easier to use concrete code (which evaluates during type checking).

Perhaps we need a feature which enables using one implementation during type checking and another at run-time. Thorsten Altenkirch asked for such a feature in the context of his and Wouter Swierstra's functional specifications of various effects.

Emacs interface

Suggested improvements:

• Have automated support to make an implicit argument explicit and visa versa;
• Make it possible to convert selected region to goal (i.e. mark with {! ... !});

Manual

Several people ask for a good manual:

Wouter

"In particular, I sometimes run into problems with implicit arguments, indexing data types by a function, modules, etc. Usually I manage to solve this by e-mailing Ulf, but I would like to see more exact specifications of what you can and cannot do. Even if it just consists of a well-documented, nicely formatted list of examples - it would make a big difference."

SamB

1. A tutorial
2. Standard library documentation (might be able to help with the tool support for this...)
3. A language/implementation reference manual in HTML and hyperlinked PDF (presumably made with LaTeX or docbook or something of that ilk) I wonder how the code in the HTML version of the manual could be kept monospace?