Idris2-boot/CONTRIBUTING.md

Contributing to Idris 2

Contributions are welcome! The most important things needed at this stage, beyond work on the language core, are (in no particular order):

• CI integration.
• Documentation string support (at the REPL and IDE mode).
• Generating HTML documentation from documentation strings (and possibly other formations)
• A better REPL, including:
  • it and :let
  • readline and tab completion
  • :search and :apropos
  • help commands
  • code colouring
• IDE mode improvements
  • Syntax highlighting support for output
  • Several functions from the version 1 IDE protocol are not yet implemented, and I haven't confirmed it works in everything.
  • (Not really part of Idris 2, but an editing mode for vim would be lovely!)
• Some parts of the Idris 1 Prelude are not yet implemented and should be added to base/
• Partial evaluation, especially for specialisation of interface implementations.
• The lexer and parser are quite slow, new and faster versions with better errors would be good.
  • In particular, large sections commented out with {- -} can take a while to lex!
• An alternative, high performance, back end. OCaml seems worth a try.
• JS and Node back ends would be nice.

The default Prelude describes the rationale for what gets included and what doesn't. Mostly what is there is copied from Idris 1, but it's not impossible I've made some silly mistakes on the way. If you find any, please let me know (or even better, submit a PR and a test case!).

Some language extensions from Idris 1 have not yet been implemented. Most notably:

• Type providers
  • Perhaps consider safety - do we allow arbitrary IO operations, or is there a way to restrict them so that they can't, for example, delete files or run executables.
• Elaborator reflection
  • This will necessarily be slightly different from Idris 1 since the elaborator works differently. It would also be nice to extend it with libraries and perhaps syntax for deriving implementations of interfaces.
• %default directives, since coverage and totality checking have not been well tested yet.

Other contributions are also welcome, but I (@edwinb) will need to be confident that I'll be able to maintain them!

If you're editing the core system, or adding any features, please keep an eye on performance. In particular, check that the libraries build and tests run in approximately the same amount of time before and after the change. (Although running faster is fine as long as everything still works :))

Libraries

Further library support would be very welcome, but unless it's adding something that was in prelude/ or base/ in Idris 1, please add it initially into contrib/. (We'll reorganise things at some point, but it will need some thought and discussion).

Think about whether definitions should be export or public export. As a general rule so far, type synonyms and anything where the evaluation behaviour might be useful in a proof (so very small definitions) are public export and everything else which is exported is export.

Syntax

Some syntax that hasn't yet been implemented but will be:

• Idiom brackets
• !-notation [needs some thought about the exact rules]

Some things from Idris 1 definitely won't be implemented:

• %access directives, because it's too easy to export things by accident
• Uniqueness types (instead, Idris 2 is based on QTT and supports linearity)
• Some esoteric syntax experiments, such as match applications
• Syntax extensions (at least in the unrestricted form from Idris 1)
• DSL blocks (probably) unless someone has a compelling use case that can't be done another way