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.
If you were on the math team during high school, you may remember integer partitions not too fondly. They're not particularly easy to get a grip on: even counting the partitions of an integer requires generating functions (which are scary when you're in high school).
Aphorisms in Haskell, using only functions in
base and with a particular bend
towards showing the use of lists for control flow. Many of these are adapted
A set of curated examples meant to show Haskell's expressiveness, wherein we write a
sum function many times: