Learn Idris by solving problems in Idris

TL;DR

• Problem list
• Playground

What is Idris

Idris is a programming language designed to encourage Type-Driven Development. (This is from the official website).

Instead of writing tests, Idris allows writing compile-time proofs that the code is correct.

What is this website

This website offers a list of problems in Idris and a service to verify the solutions are correct. It is like leetcode for Idris.

The problems on this website are type-checked mostly. They are not executed, there are only few tests in basic excersices. The idea is: if the code is successfully type-checked, then it works correctly. Of course, it is a very idealistic world view, but anyway, this website only tries to help to learn dependent types, not algorithms.

Most of the problems were taken from:

• Type-driven development with Idris book by Edwin Brady, the author and maintainer of the Idris language and implementation
• Verified Functional Programming in Agda by Aaron Stump. Agda and Idris are both dependently-typed programming languages, with very similar semantics but quite different syntaxes. Agda relies heavily on Unicode, while Idris is very similar (syntactically) to the Haskell. Anyway, the book is also a good introduction to dependent types.
• Idris standard library contains a lot of algorithms, reimplementation of these algorithms could be a good exercise. For example, proofing that plus operation is commutative for natural numbers is less than 10 lines of code, but could take quite a lot of time for people new dependent types.
• Have an idea of a good problem? Send us an e-mail.

Something doesn't work?

There's a github project with issue tracker.

Problems

The list