Idris (programming language)
| Paradigm | Functional |
|---|---|
| Designed by | Edwin Brady |
| Stable release | 0.9.7
/ March 10, 2013 |
| OS | Cross-platform |
| License | BSD-3 |
| Filename extensions | .idr |
| Website | Idris website |
| Influenced by | |
| Agda, Epigram, Haskell, ML, Coq | |
Idris is a general-purpose pure functional programming language with dependent types. The type system is similar to the one used by Agda.
The language supports interactive theorem-proving compareable to Coq, including tactics, while the focus remains on general-purpose programming even before theorem-proving. Other goals of Idris are "sufficient" performance, easy management of side-effects and support for implementing embedded domain specific languages.
Currently, Idris compiles to C and relies on the Boehm garbage collector. There also exists a JavaScript backend.
References
- Brady: IDRIS — Systems Programming Meets Full Dependent Types, PLPV 2012 http://www.cs.st-andrews.ac.uk/~eb/writings/plpv11.pdf
- Brady: Programming in Idris: a tutorial http://www.cs.st-andrews.ac.uk/~eb/writings/idris-tutorial.pdf
- Brady, Hammond: Resource-safe Systems Programming with Embedded Domain Specific Languages, PADL 2012 http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf
External links
- The Idris homepage, including documentation, frequently asked questions and examples
- Idris at the Hackage repository
- Idris Tutorial