blog

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.