Other interesting ones to look at are F* (a joint effort from Microsoft Research and INRIA to create an ML-like dependently typed language) and ATS (a low-level, fast dependently typed language meant to replace C). What's cool about both of these is that they put emphasis on allowing imperative programming despite being dependently typed and seeming very functional.
Comments
If you are interested in Idris, you might also be interested in agda, which is another dependently typed programming language: https://en.wikipedia.org/wiki/Agda_(programming_language)
Other interesting ones to look at are F* (a joint effort from Microsoft Research and INRIA to create an ML-like dependently typed language) and ATS (a low-level, fast dependently typed language meant to replace C). What's cool about both of these is that they put emphasis on allowing imperative programming despite being dependently typed and seeming very functional.