Idris is a general-purpose, purely functional programming language that supports dependent types and lazy evaluation.
Designed by Edwin Brady in 2007, the language was influenced by Haskell, with which it shares several features, particularly syntax and types, although Idris has a more advanced type system. Its type system also has similarities with Agda, and its proofs can be compared to Coq. Although it was designed as a general-purpose language, Idris can also be used as a proof assistant. Dependent types are powerful enough to encode most properties of programs and, since an Idris program can prove invariants at compile-time, it has the qualities of a proof assistant.
There are also influences from Clean, Epigram, the ML languages, and Rust.
Still in development by the Idris Community, Idris 2 is expected to have a Chez Scheme backend, which is an implementation of the Scheme programming language, and part of the Lisp family of languages.
Idris will compile to C using a simple foreign function interface.
The continued development of Idris is carried out by the Idris Community, under the leadership of Edwin Brady at the University of Saint Andrews. The language is open-source, using the BSD License.
The focus of this guide is on the Idris programming language, although any editors, IDEs, or other tools designed to facilitate programming in Idris are also appropriate for this category, as are any Idris user groups, forums, tutorials, or guides.
Recommended Resources
Documentation for the Idris Language
Published under the Creative Commons CCO License, the official documentation for the programming language, as prepared by the Idris Community, and provided by Read the Docs, is presented. Included is a tutorial for Idris users, answers to frequently asked questions (FAQs), a paper on implementing state-aware systems in Idris, a tutorial on effects, and on the language’s use in theorem proving, as well as language references, and other guides for its use.
http://docs.idris-lang.org/en/latest/
Written and maintained by Edwin Brady, the author and chief development lead for the Idris programming language, the site posts informational articles relating to the language, as written by Brady or others whose work he has chosen to share. The larger site includes topics, mostly of a programming nature, such as dependent types, domain-specific languages, and hacks. Various papers on similar topics are also featured, with a synopsis and PDF of the full article.
https://edwinb.wordpress.com/category/idris/
As of this writing, this is a pre-alpha implementation of Idris 2, the successor to Idris. Mostly backward compatible with Idris 1, there are some exceptions, which are discussed here, along with the new features that have been added, comments on features still missing, and installation instructions. Packages for Idris 2 are available to be downloaded or cloned, including documentation. Licensure information is noted, and the list of contributors is acknowledged.
https://github.com/edwinb/Idris2
The official website of the Idris Community features the Idris programming language, offering an overview of the language, its purposes, features, and community support information. Development notes and version announcements are posted, and examples of Idris data types and syntax are included, along with a tutorial on the language, on implementing state-aware systems, and specific features. API documentation and community contributions and standards are featured.
https://www.idris-lang.org/
Idris: Functional Programming Language with Dependent Types
Hosted on Hackage, the Haskell community’s central package archive of open-source software, this section of the site features development versions of the Idris programming language, including full packages, modules, changelogs, and dependencies. A brief overview of the language and information about its licensure, author, maintainer, and links to the official language site, bug trackers, source repositories, and other resources are included.
http://hackage.haskell.org/package/idris
