Practical examples of Idris

Question

Are there any examples of Idris that might be used to study and perhaps apply it for general purpose/"real world" application?

I am moderately proficient in Haskell, of which Idris seems to borrow significantly, and the official FAQ/documentation is rather nice but it would be very helpful to have some larger examples to explore. The goal is attempting to use Idris for practical software development. TIA.

Answer 1

Edwin Brady has a repo full of demos at https://github.com/edwinb/idris-demos. Among other things, it has a playable space invaders game, written using SDL bindings, Effects, and the !-effect syntax (basically an alternate syntax to do-notation / >>=).

Also, we attempt to maintain a listing of some available libraries on the wiki: https://github.com/idris-lang/Idris-dev/wiki/Libraries

Answer 2

There is a paper by Edwin Brady, the creator of Idris, which deals with real world questions such as efficiency and concurrency: "Correct-by-Construction Concurrency: using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols". It not only explains how to deal with concurrency, but also creates an embedded domain specific language (EDSL) in Idris to deal with concurrency.

It is also used for scientific computing (which may or may not qualify as real world application): Dependently-typed programming in scientific computing. The paper contains actual examples and a few Agda examples as well.

Update 2022: There's also an awesome list at github now.