I've been using Idris for a while, and today I stumbled into an example of a dynamorphism that worked so beautifully I had to share. It is a stellar example not only of dependent types but also the rĂ´le abstraction can play in writing correct code.

The example code below uses my recursion_schemes library, along with a dynamorphism-based computation of the Catalan numbers taken from a paper of Hinze and Wu.

import Data.Functor.Foldable import Data.Functor.Foldable.Instances import Data.Functor.Foldable.Exotic import Control.Comonad.Cofree

catalan : Nat -> Nat catalan = dyna coalgebra naturals where coalgebra : ListF Nat (Cofree (ListF Nat) Nat) -> Nat coalgebra NilF = 1 coalgebra (Cons n table) = sum (Prelude.List.zipWith (*) xs (reverse xs)) where xs = take n table take : Nat -> (Cofree (ListF Nat) Nat) -> List Nat take Z _ = [] take (S n) (Co a NilF) = [a] take (S n) (Co a (Cons v as)) = a :: take n as

Idris gives a particularly elegant way to interact with free comonads. Thanks to its ability to disambiguate names, we can write take without clashing with the prelude.