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.
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 | next