Recursion schemes

Recursion schemes for Idris

From vmchale·Updated August 15, 2025·View on GitHub·

This is a library providing recursion schemes for Idris. It it is loosely based on Edward Kmett's [Haskell library](https://hackage.haskell.org/package/recursion-schemes). The project is written primarily in Idris, distributed under the BSD 3-Clause "New" or "Revised" License license, first published in 2017. Key topics include: control-flow, idris, idris-ecosystem, recursion, recursion-schemes.

recursion_schemes

This is a library providing recursion schemes for Idris. It it is loosely based
on Edward Kmett's Haskell
library.

Installation

First, install idris-free,
comonad and composition. Then:

idris --install recursion_schemes.ipkg

To run the tests, install specdris.
Then:

idris --testpkg test.ipkg

Use

The classic paper Functional programming with bananas, lenses, envelopes and
barbed wire is the
inspiration behind the Haskell library and is the standard reference on the
topic. You may also find Law and Order in
Algorithmics
to be of use.

Examples

In the Test.Spec module there are several examples, including a catamorphism,
a zygomorphism, a mutumorphism, an Elgot algebra, a paramorphism, a
dynamorphism, and a hylomorphism.