A Dependently Typed Functional Programming Language
Idris (http://idris-lang.org/) is an experimental functional programming language with dependent types. To install, type 'make'. This will install everything using cabal and typecheck the libraries.