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 Programming with Effects
- Some Reference Materials (this is not complete)
- Some tutorials on specific features
Documentation is also available in EPUB format.
There is also a book in development, titled Type Driven Development in Idris.
There is API documentation for the following packages provided as part of the Idris distribution:
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 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
- 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.