Idris is a functional programming language with dependent types.