Download
Idris‑dev is the development version of Idris 1, a general-purpose functional programming language featuring full dependent types, designed for writing type-safe programs and proofs within the language itself. It compiles to C and JavaScript (for Node.js and browsers), and supports code generation via substitute backends. This repository represents the latest development version of the language, and may contain bugs that are being actively worked on. For those who wish to use a more stable version of Idris please consider installing the latest version that has been released on Hackage. Installation instructions for various platforms can be found on the Idris Wiki. Idris has support for external code generators. Supplied with the distribution is a C code generator to compile executables, and a JavaScript code generator with support for node.js and browser JavaScript.
Features
- Full dependent types allowing values to appear in types
- Totality checking to ensure functions are complete and terminating
- Code generators for C and JavaScript (browser and Node.js)
- Supports external backends (e.g., JVM, CIL, LLVM) via community contributions
- Strong type-driven development inspired by proof assistants like Agda and Coq
- Actively maintained in parallel with Idris 2 development
Project Samples
