Idris

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

0 Mentors

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

44 Students

Join hundreds of 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

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
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)

Exercism is a great website

What I like about it is that I am able to solve the challenges in a TDD way working in a environment that I am familiar (my own PC not a browser IDE) and the cherry on the top of the cake is that I have access to code reviews.

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
Hello World
easy
optional values
text formatting
Hamming
easy
export modifiers
vectors
Accumulate
easy
functions
lists
map

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

Join the Idris Track