Hacker News Reader

Jan Corazza has some really great write-ups about writing bindings to SDL and writing a video game in Idris using them. The source is available on Github

I wrote a Todo application in Idris that compiles to Javascript (https://github.com/leon-vv/Todo). I used the dependent type system of Idris to embed a small part of SQL in Idris, which means the type system can proof certain things about my queries (for example that fields accessed are actually part of the (joined) tables).

Idris is primarily an academic language, much like Haskell. While I don't doubt that people will come to implement such programs in it at some point, I haven't seen anything yet (though I admittedly don't stick close to Idris at the moment so I could've missed something).