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.Cofreecatalan : 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.