Documentation for Idris is available from docs.idris-lang.org. This currently includes:

• A Tutorial, introducing the language and its main features
• Frequently Asked Questions with answers
• A tutorial on Implementing State-aware Systems
• Some Reference Materials (this is not complete)
• Some tutorials on specific features

Documentation is also available in EPUB format.

There is also a book, titled Type Driven Development in Idris and published by Manning.

There is API documentation for the following packages provided as part of the Idris distribution:

• prelude
• base
• contrib
• effects

There is also brief documentation on the packaging system for Idris libraries, and the effects package.

The Idris wiki contains lots of community supplied information, in particular a manual is developing.

There is also an FAQ. If you have a question which isn’t answered in the FAQ, please don’t hesitate to ask.

Note that at the moment, development is moving quickly, and as a result there are several features for which documentation is somewhat spotty. The mailing list and the Freenode channel are active and helpful, however, if you get stuck, and once you learn something that you did not find in the documentation, do consider contributing to the tutorial or to the wiki manual!

Other Publications

Other publications associated with Idris are as follows:

• Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation, Edwin Brady
  Accepted for publication in Journal of Functional Programming, August 2013. To appear.
• Dependent Type Providers, David Christiansen
  In proceedings of WGP 2013
• Programming and Reasoning with Algebraic Effects and Dependent Types, Edwin Brady
  In proceedings of ICFP 2013
• Sequential decision problems, dependently typed solutions, Nicola Botta, Cezar Ionescu and Edwin Brady
  In proceedings of PLMMS 2013
• Programming in Idris: a tutorial, Edwin Brady
  January 2012
• Resource-safe Systems Programming with Embedded Domain Specific Languages, Edwin Brady and Kevin Hammond
  Revised version to appear in PADL 2012
• Idris – Systems Programming meets Full Dependent Types, Edwin Brady
  In PLPV 2011.
• Scrapping your Inefficient Engine: using Partial Evaluation to Improve Domain-Specific Language Implementation, Edwin Brady and Kevin Hammond
  In ICFP 2010.
• Correct-by-Construction Concurrency: using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols, Edwin Brady and Kevin Hammond
  In Fundamenta Informaticae, Volume 102, 2010.
• Domain Specific Languages (DSLs) for Network Protocols, Saleem Bhatti, Edwin Brady, Kevin Hammond and James McKinna.
  In NGNA 2009.
• Lightweight Invariants with Full Dependent Types, Edwin Brady, Christoph Herrmann and Kevin Hammond.
  In proceedings of TFP 2008.