Idris

Join the Idris Track
TODO: The maintainers have not provided a description for this track.
Join the Idris Track
Track mentors

0 Mentors

Our mentors are friendly, experienced Idris developers who will help teach you new techniques and tricks.
Track students

49 Students

Join the many students who have enjoyed learning and improving their skills by taking this track.
Track exercises

5 Exercises

Hundreds of hours have gone into making these exercises fun, useful, and challenging to help you enjoy learning.

About Idris

module EvenOdd

data Even : Nat -> Type where
  EZ : Even Z
  ES : Even n -> Even (S (S n))

total
ee : Even n -> Even m -> Even (n + m)
ee EZ m     = m
ee (ES n) m = ES (ee n m)

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
Join the Idris track

A tremendous learning opportunity to explore the depth of your own knowledge

Exercism is fantastic in learning new languages but that is not the extent of it. If you are a "more experienced" programmer you may have encountered impostor syndrome: the idea you don't really know what you think you know. Exercism lets you solve problems and put them in the space of open feedback which is a tremendous learning opportunity to explore the depth of your own knowledge. Even if you have been programming in a language for awhile it is worth checking into Exercism to see where you stand with current implementation practices.

Fun. Challenging. Interesting

Community-sourced Idris exercises

These are a few of the 5 exercises on the Idris track. You can see all the exercises here.

RNA Transcription
easy
pattern matching
vectors
Leap
easy
arithmetic
booleans
integers
Accumulate
easy
functions
lists
map
Hamming
easy
export modifiers
vectors
Hello World
easy
optional values
text formatting

Get started with the Idris track. As with everything on Exercism, it's 100% free!

Join the Idris Track