For those curious what Idris is, from http://www.idris-lang.org/ : "Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type."
Here's a couple of talks about Idris:
Edwin Brady at London Haskell: https://www.youtube.com/watch?v=vkIlW797JN8
David Christiansen at Haskell DC: http://bmsherman.github.io/idris-drc-3-26-14/
And there's a tutorial and other docs available here: http://www.idris-lang.org/documentation/