Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. We demonstrate how to encode functional and relational derivations in a dependently typed programming language. A program is coupled with an algebraic derivation from a specification, whose correctness is guaranteed by the type system. Code accompanying the paper has been developed into an Agda library AoPA.
Catamorphisms Folding data structures An overview and derivation of the category-theoretic notion of a catamorphism as a recursion scheme, and an exploration of common variations on the theme. Catamorphism, A Field Guide to Recursion Schemes: Catamorphism Contents lessmore SharePrintPrintFavoriteFavorite Description Catamorphisms are generalizations of the concept of a fold in functional programming. A catamorphism deconstructs a data structure with an F-algebra for its underlying functor. History The name catamorphism appears to have been chosen by Lambert Meertens [1]. The category theoretic machinery behind these was resolved by Grant Malcolm [2][3], and they were popularized by Meijer, Fokkinga and Paterson[4][5]. The name comes from the Greek 'κατα-' meaning "downward or according to". A useful mnemonic is to think of a catastrophe destroying something.