Structured recursion schemes have been widely used in constructing, optimizing, and reasoning about programs over inductive and coinductive datatypes. Their plain forms, catamorphisms and anamorphisms, are restricted in expressivity. Thus many generalizations have been proposed, which further led to several unifying frameworks of structured recursion schemes. However, the existing work on unifying frameworks typically focuses on the categorical foundation, and thus is perhaps inaccessible to practitioners who are willing to apply recursion schemes in practice but are not versed in category theory. To fill this gap, this expository paper introduces structured recursion schemes from a practical point of view: a variety of recursion schemes are motivated and explained in contexts of concrete programming examples. The categorical duals of these recursion schemes are also explained.
When modelling side-effects using a monad, we need to equip the monad with effectful operations. This can be done by not-ing that each algebra of the monad carries interpretations of the desired operations. We consider the analogous situation for graded monads, which are a generalization of monads that enable us to track quantitative information about side-effects. Grading makes a significant difference: while many graded monads of interest can be equipped with similar operations, the algebras often cannot. We explain where these operations come from for graded monads. To do this, we introduce the notion of flexibly graded monad, for which the situation is similar to the situation for ordinary monads. We then show that each flexibly graded monad induces a canonical graded monad in such a way that operations for the flexibly graded monad carry over to the graded monad. In doing this, we reformulate grading in terms of locally graded categories, showing in particular that graded monads are a particular kind of relative monad. We propose that locally graded categories are a useful setting for work on grading in general.
Where do datastructures come from? This paper explores how to systematically derive implementations of one-sided flexible arrays from a simple reference implementation. Using the dependently typed programming language Agda, each calculation constructs an isomorphic—yet more efficient—datastructure using only a handful of laws relating types and arithmetic. Although these calculations do not generally produce novel datastructures they do give insight into how certain datastructures arise and how different implementations are related.
Subtypes are useful and ubiquitous, allowing important properties of data to be captured directly in types. However, the standard encoding of subtypes gives no control over when the reduction of subtyping proofs takes place, which can significantly impact the performance of type-checking. In this article, we show how operations on a subtype can be represented in a more efficient manner that exhibits no reduction behaviour. We present the general form of the technique in Cubical Agda by exploiting its support by higher-inductive types, and demonstrate the practical use of the technique with a number of examples.
Functional programs with side effects represented by monads are amenable to equational reasoning. This approach to program verification has been experimented several times using proof assistants based on dependent type theory. These experiments have been performed independently but reveal similar technicalities such as how to build a hierarchy of interfaces and how to deal with non-structural recursion. As an effort towards the construction of a reusable framework for monadic equational reasoning, we report on several practical improvements of Monae, a Coq library for monadic equational reasoning. First, we reimplement the hierarchy of effects of Monae using a generic tool to build hierarchies of mathematical structures. This refactoring allows for easy extensions with new monad constructs. Second, we discuss a well-known but recurring technical difficulty due to the shallow embedding of monadic programs. Concretely, it often happens that the return type of monadic functions is not informative enough to complete formal proofs, in particular termination proofs. We explain library support to facilitate this kind of proof using standard Coq tools. Third, we augment Monae with an improved theory about nondeterministic permutations so that our technical contributions allow for a complete formalization of quicksort derivations by Mu and Chiang.
