Idris 2

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

Installation and Packages

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.

Resources to Learn Idris 2

Books

• Type-Driven Development with Idris, Edwin brady. This was written for Idris1. If you are using Idris2, you should make these changes

Tutorials

• Functional Programming in Idris 2
• A Tutorial on Elaborator Reflection in Idris 2, accompanied by library utilities
• An attempt at explaining Decidable Equality

Official talks

• 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

Community talks

• 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

Documentation

• Official documentation
• Standard library online API reference
  • official, latest
  • community
• Community API reference for selected packages

Docker images

• 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

Things still missing

• Cumulativity (currently Type : Type. Bear that in mind when you think you've proved something)
• rewrite doesn't yet work on dependent types

Contributions wanted

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.