My department currently has a course on "Functional Programming" using Haskell. The goal of this little project is to take the Haskell code and reimplement it in a dependently typed language (for now Agda, but I want to try Idris as well) to, for example, encode invariants directly. Hopefully, we can then use the material in the upcomming term to impress students with these wonderful languages.