Idris is a dependently typed purely functional programming language influenced by Haskell. See http://idris-lang.org