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 https://github.com/exercism/idris/issues if you have suggestions, or submit a patch with improvements to the https://github.com/exercism/idris/blob/master/docs/ABOUT.md 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.

1
exercism fetch idris

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

1
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.

1
exercism submit PATH_TO_FILE