Contributions Needed

If you’re interested in contributing to Idris, there are several jobs and mini-projects which would help. For example:

Package Management and Libraries

There are now several packages out there, but no canonical way to find them. We also have a (very simple) packaging system that allows individual packages to be installed. It would be useful to have a packaging system that dealt with dependencies, installed necessary dependencies, provided an index on the web, and worked portably on as many platforms as possible.

For common libraries (e.g. networking, web programming common data formats such as JSON and XML, parsing) it would be nice for Idris to come "batteries included". That is, we should provide good default libraries for these common tasks (via C bindings if necessary, but better if they're portable across back ends).

Total Parser Library

There is a parser library lightyear which has proved useful for small problems, but it has several limitations. We would like a complete parser library with support for different token types, line/column numbers, whitespace significance, parsing expressions with precedence rules, and which provides good error messages. Ideally, it would also be compatible with Control.ST to allow parsers to easily have state and other effects if necessary.

It should also make it easy (or at least possible) to write total parsers. Using Nils Anders Danielsson's total parser combinators (from Agda) as a starting point seems a good idea.

In June 2017, Text.Parser was added.

LLVM Code Generation

Or, indeed, any form of code generation which aims at a fast run time (such as via Malfunction). The C back end is a useful reference back end because it's small, and doesn't introduce any complications with installation. However, there are several fundamental limitations with using C as a target language and so it would be nice to have a target which specifically aimed to be fast.

Distribution of Idris and its Libraries

We distribute Idris as source, via hackage, and as an OSX binary package generated from a script. Then, volunteers produce packages for Windows and Homebrew. There is almost certainly a better way for us to package things up, if anyone has any knowledge of how to do that well...

Javascript Code Generation

While we do have a working Javascript code generator, it needs a maintainer. It might also be a good idea to try some other strategies, starting from different intermediate forms. Also, to show its value, what can we do with it? How about an Idris-like architecture for single page applications in Javascript? (Yes, a Framework :))

In May 2017, a new JS backend based on liftDecls was added by rbarreiro and be5invis.

Library Documentation Generation

Again, this works, but it could use some attention. Most usefully, ordering documentation by where things appear in code, rather than the current reverse alphabetical order (which seems to be an effect of Data.Map) and providing links to source code from documentation. This could ideally be integrated with a package manager (e.g. consider how hackage shows APIs)

Better concurrency support

The C back end has a simple implementation of message passing concurrency, which is good enough for experimental purposes, but is not fast. It would be good to have much better concurrency support at run time - this may involve changing the run time system a lot (or even writing a new one).

Related, but not quite the same: there is no support at the moment for parallel computation.

Polishing the Network Libraries

There is a Network.Sockets library in contrib. which covers the basics. This has been fine for experimental purposes, but it hasn't been used extensively in practice. Using it to provide implementations of common protocols (e.g. HTTP, DNS, SMTP...) would be useful both to test the library, and because these would be useful in their own right. Also, support for TLS would be very nice to have.

Completing the Reference Documentation

We have a man page, covering the command line options, and there is help at the REPL. There is also a start at documenting every language feature (experimental or otherwise) at http://docs.idris-lang.org/ but this needs filling out.

Working towards self-hosting

I'm including this because it needs doing eventually, even if it's a huge job that is unlikely to be done any time soon. There are a lot of things in the current implementation which result from bad implementation decisions (either things optimising for getting an implementation done faster, or things resulting from not really knowing what we were doing yet...) and that are hard to change no matter how much we want to. A few things limit how fast the type checker can be, unnecessarily.

Many of the above things will help with work towards self hosting, but keeping it in mind as a goal will be a good idea.

Improving expression search

The interactive expression search feature (for filling holes automatically in an editor) currently replaces a hole with the first result it finds via a brute force search. As useful as this can be, it would be much better if, instead, it presented a list of possible solutions in case the first result is not what's required. There are other possible improvments too: it's not good at finding recursive solutions except in some special circumstances because it doesn't try to work out what the valid recursive calls are; it would be nice to display multiple partial solutions if it can't find a complete solution; and (much harder!) it doesn't know about case splitting so it can't find complete function definitions even if there is one obvious one (e.g. it ought to be able to find append on vectors with one keystroke).

Port the REPL to Idris

Idris's interactive command-line interface is written in Haskell. A good start towards self-hosting would be to replace this with one written in Idris itself that communicates over the same protocol used by Emacs and Atom.

More work on linear types

There is an experimental implementation of linear types, but it's some way from being usable in practice. Linear types would be useful for a number of reasons, in particular to allow precise control of memory management in low level situations.

Other suggestions

What follows is a list of smaller suggestions which used to be the content of this page. While a lot of this is subsumed by the ideas listed above, several may still inspire potential contributors:

Libraries

• Adding libraries and functions to the base package.
• Low level bindings for various C APIs, including, but not limited to:
  • Network sockets
  • libgcrypt
  • libSDL
• High level, more dependently typed bindings for the above.

Documentation & Examples

• Expand the tutorial with detailed examples and exercises (or even writing a new one)
• Add to the reference documentation.
• Checking for documentation rot in the Idris libraries (see libs/), and Haskell implementation in src.

Internals

• Compiler support for "go to definition" in editors
• Improving the termination and productivity checkers. The current version works in principle, but has a number of issues which need addressing.
• Proof automation, for example:
• A Presburger arithmetic solver (in progress here).
• Commutative ring rewriting (in progress here)

Developer Experience

• Implement something like Interlisp's DWIM for fixing type errors
• Generation of project stubs or "skeleton projects" like those produced by, e.g., stack new. Provide support for generation of project stubs for: new backends, Idris library, Idris binary.
• Flag to generate ignore files for Git and Mercurial.
• Flag to show paths
• Improve Idris docs for algebraic data types.

Bug Squashing

• Investigating and fixing the reports on the issue tracker (low-hanging fruit designates issues that we believe to be easier than others)

Distribution

• Polishing the packaging system
• Packaging for Mac, for ease of installation (ideally not requiring a Haskell platform installed)
• Packaging for Linux distributions

Testing and Benchmarks

• Create Idris versions of toy programs for the benchmark game
• Write a comprehensive suite for backends to test against that covers all primitives to ensure uniformity.