Idris Language

Idris is a general purpose pure functional programming language with dependent types. Idris has C++ (and PHP!) backends.

“Type driven development” is the book written by the creator of Idris – Edwin Brady espousing the benefits dependent types.

10 things Idris improved over Haskell – Deque [Jun 2017].

Notes on Idris – The Breakfast Post