Mini Projects

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

• Adding libraries and functions to the base package.
• 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.
• Expanding the tutorial with detailed examples and exercises (or even writing a new one)
• Investigating and fixing the reports on the issue tracker (low-hanging fruit designates issues that we believe to be easier than others)
• 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.
• Polishing the packaging system
• Proof automation, for example:
• A Presburger arithmetic solver (in progress here).
• Commutative ring rewriting (in progress here)
• Packaging for Mac, for ease of installation (ideally not requiring a Haskell platform installed)
• Packaging for Windows
• Create Idris versions of toy programs for the benchmark game
• Implement something like Interlisp's DWIM for fixing type errors
• Checking for documentation rot in the Idris libraries (see libs/), and Haskell implementation in src.
• Implement Numerical syntax sugar for Fin types