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.
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:
plusoperation 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.
There's a github project with issue tracker.