Learn Idris by solving problems in Idris


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:

Something doesn't work?

There's a github project with issue tracker.


The list