Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type. It is compiled, with eager evaluation. Its features are influenced by Haskell and ML, and include:

  • Full dependent types with dependent pattern matching
  • Simple foreign function interface (to C)
  • Compiler-supported interactive editing: the compiler helps you write code using the types
  • where clauses, with rule, simple case expressions, pattern matching let and lambda bindings
  • Dependent records with projection and update
  • Interfaces (similar to type classes in Haskell)
  • Type-driven overloading resolution
  • do notation and idiom brackets
  • indentation significant syntax
  • Extensible syntax
  • Cumulative universes
  • Totality checking
  • Hugs style interactive environment

Help us explain this better! File a GitHub issue at if you have suggestions, or submit a patch with improvements to the file.

Try It!

If you've downloaded the command-line client and have Idris installed on your machine, then go ahead and fetch the first problem.

exercism fetch idris

In order to be able to submit your solution, you'll need to configure the client with your Exercism API key.

exercism configure --key=YOUR_EXERCISM_KEY

When you've written a solution, submit it to the site. You'll have to configure the command-line client with your exercism API key before you can submit.

exercism submit PATH_TO_FILE