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