github.com/idris-lang/idris2 ↗

About idris-lang/idris2

Idris 2 is a purely functional programming language with first-class types, designed around dependent type theory. The language emphasizes type-driven development, where types can be computed and manipulated like values, enabling developers to encode invariants directly into the type system. The compiler and runtime are written in Idris itself, showcasing a bootstrapped implementation of the language concepts.

The project provides a complete development ecosystem including a compiler, standard library, package manager called pack, and extensive documentation. The community has contributed editor support, Docker images, and multiple tutorials and learning resources. The wiki maintains a curated collection of third-party libraries and links to official talks that demonstrate the language's capabilities in areas like data science, backend development, and type-driven design patterns.

The project remains under active development with known limitations including the absence of cumulativity in the type hierarchy and incomplete support for rewriting on dependent types. The maintainers actively seek contributions from the community through labeled issues for newcomers and more experienced contributors, providing documentation and source code guides to help prospective developers navigate the codebase.