Idris 2 is a purely functional programming language with first class types.
For installation instructions, see INSTALL.md.
The wiki lists a number of useful resources, in particular
- What's changed since Idris 1
- Resources for learning Idris, including official talks that showcase its capabilities
- Editor support
The most common way to install the latest version of Idris and its packages is through pack Idris' package manager. Working with the latest version of Idris is as easy as pack switch latest.
Follow instructions on the pack repository for how to install pack.
To use pack and idris, you will need an .ipkg file (Idris-package file) that describes your idris project.
You can generate one with idris2 --init. Once setup with an .ipkg file, pack gives you access to the pack collection of packages, a set of compatible libraries in the ecosystem.
If your dependency is in the depends field of your .ipkg file, pack will automatically pull the dependency from you matching pack collection.
The wiki hosts a list of curated packages by the community.
Finally, pack also makes it easy to download, and keep updated version of, idris2-lsp, and other idris-related programs.
- Type-Driven Development with Idris, Edwin brady. This was written for Idris1. If you are using Idris2, you should make these changes
- Functional Programming in Idris 2
- A Tutorial on Elaborator Reflection in Idris 2, accompanied by library utilities
- An attempt at explaining Decidable Equality
- What's New in Idris 2, Edwin Brady, Berlin Functional Programming Group
- Scheme Workshop Keynote, Edwin Brady, ACM SIGPLAN
- Idris 2 - Type-driven Development of Idris, Edwin Brady, Curry On! 2019
- Idris 2: Type-driven development of Idris, Edwin Brady, Code Mesh LDN 18
- The implementation of Idris 2, Edwin Brady, SPLV'20 and accompanying code
- Domain Driven Design Made Dependently Typed, Andor Penzes, Aug '21
- Extending RefC - Making Idris 2 backends while avoiding most of the work, Robert Wright, Sept '21
- Introduction to JVM backend for Idris 2, Marimuthu Madasamy, Oct '21
- Idris Data Science Infrastructure - Because sometimes we have to consider the real world, Robert Wright, Dec '21
- Official documentation
- Standard library online API reference
- Community API reference for selected packages
- Multi-arch, multi-distro Docker images for Idris 2
- Official images for the Pack package manager
- alexhumphreys/idris2-dockerfile
- mattpolzin/idris-docker
- dgellow/idris-docker-image
- Cumulativity (currently
Type : Type. Bear that in mind when you think you've proved something) rewritedoesn't yet work on dependent types
If you want to learn more about Idris, contributing to the compiler could be one way to do so. The contribution guidelines outline the process. Having read that, choose a good first issue or have a look at the contributions wanted for something more involved. This map should help you find your way around the source code. See the wiki page for more details.