Practical examples of Idris

43
votes

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.

2
dependent-typeidris
I am also in a similar position, relatively proficient in Haskell (understand GADT's, Type Families, etc...) and looking to explore full dependent types in Idris. It would be nice to fine some more examples. – MFlamer
Just for reference, here is a related question about real-world agda programs (unfortunately closed). – Joachim Breitner

2 Answers

28
votes

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

17
votes

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.