Idris 0.12
Idris is a functional programming language with dependent types, where values are constrained and pattern-matched by an expressive type system to avoid logic misbehaviours. It's a general purpose language, but also supports interactive theorem-proving, is sufficient performant trough eager and LLVM compilation. It has monads, type classes, comprehensions, lambda bindings, where and with clauses, expressions in case statements, an indendation-based and extendable syntax, lists, tuples and pairs,