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).
A set of curated examples meant to show Haskell's expressiveness, wherein we write a sum function many times:
As you may have read in one of my past posts or elsewhere, performance across languages can be complicated, and it's not always as obvious as you'd expect.
I came across the idea to use \(F\)-(co)algebras to encode general constructors and destructors when reading Martin Erwig's paper on synchromorphisms.
prev | next