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'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.
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.
The modern theory of continued fractions comes from Christiaan Huygens, a Dutch physicist who invented the pendulum clock. Continued fractions turn out to be an especially elegant way of finding rational approximations of a number; this enabled him to design clocks with small gears that nonetheless provided the desired degree of accuracy.
prev