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."
I'll add: if all this seems too opaque to jump into at once (and especially if you're unfamiliar with Haskell or other FP languages), don't give up on FP!
A "functional" language is not always a "pure" language, and a "pure functional" language certainly does not always have dependent types. These concepts build on each other.
A great intro to FP is "Programming in Standard ML". Concise, precise, and very approachable. SML is functional, but not pure nor dependently-typed (though purity is encouraged). http://www.cs.cmu.edu/~rwh/smlbook/book.pdf
Haskell is like SML with enforced purity, a different module/typeclass system, and default laziness. LYAH is the best intro. http://learnyouahaskell.com/
Idris is aimed primarily at those already familiar with Haskell, so don't be discouraged if the online REPL feels too foreign!
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/