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.