Skip to content
<awesome-gh-repos>
vic

idris-lang/Idris2

A purely functional programming language with first class types
Source code at GitHub https://idris-lang.org/
idris-lang/Idris2.json
{
  "createdAt": "2020-05-17T23:25:25Z",
  "defaultBranch": "main",
  "description": "A purely functional programming language with first class types",
  "fullName": "idris-lang/Idris2",
  "homepage": "https://idris-lang.org/",
  "language": "Idris",
  "name": "Idris2",
  "pushedAt": "2025-11-25T16:14:32Z",
  "stargazersCount": 2776,
  "topics": [
    "compiler",
    "dependent-types",
    "hacktoberfest"
  ],
  "updatedAt": "2025-11-25T22:31:51Z",
  "url": "https://github.com/idris-lang/Idris2"
}

Idris 2

Section titled “Idris 2”

Documentation Status Build Status

Idris 2 is a purely functional programming language with first class types.

For installation instructions, see [INSTALL.md]!(INSTALL.md).

The wiki lists a number of useful resources, in particular

Installation and Packages

Section titled “Installation and Packages”

The most common way to install the latest version of Idris and its packages is through [pack][PACK] Idris’ package manager. Working with the latest version of Idris is as easy as pack switch latest. Follow instructions [on the pack repository][PACK] 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][PACK_COL] 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

Section titled “Resources to Learn Idris 2”

Books

Section titled “Books”

Tutorials

Section titled “Tutorials”

Official talks

Section titled “Official talks”

Community talks

Section titled “Community talks”

Documentation

Section titled “Documentation”

Docker images

Section titled “Docker images”

Things still missing

Section titled “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

Section titled “Contributions wanted”

If you want to learn more about Idris, contributing to the compiler could be one way to do so. The [contribution guidelines]!(CONTRIBUTING.md) outline the process. Having read that, choose a [good first issue][1] or have a look at the [contributions wanted][2] for something more involved. This [map][3] should help you find your way around the source code. See [the wiki page][4] for more details.

[1] !: https://github.com/idris-lang/Idris2/issues?q=is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22 [2] !: https://github.com/idris-lang/Idris2/wiki/What-Contributions-are-Needed [3] !: https://github.com/idris-lang/Idris2/wiki/Map-of-the-Source-Code [4] !: https://github.com/idris-lang/Idris2/wiki/Getting-Started-with-Compiler-Development [PACK] !: https://github.com/stefan-hoeck/idris2-pack [PACK_COL] !: https://github.com/stefan-hoeck/idris2-pack-db