I wanted to share a little example I came across while working on one of my Idris libraries. It's matrix multiplication, but from an angle you may not be used to. In particular, though it is written in Idris (a strict language), it composes as well arrays in Haskell or another lazy language thanks to dependent types.
One way to define laziness is as follows: a language has strict evaluation if and only if \(f(\bot) = \bot\) for every function \(f\) definable in the language.
I recently wrote tomlcheck, which, as the name implies, is a syntax checker for TOML files. Since I'd read a call-to-arms regarding the lack of concrete success stories in Haskell a few months ago, I figured I'd contribute one of mine.
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).
prev | next