We study Kleene iteration in the categorical context. A celebrated completeness result by Kozen introduced Kleene algebra (with tests) as a ubiquitous tool for lightweight reasoning about program equivalence, and yet, numerous variants of it came along afterwards to answer the demand for more refined flavors of semantics, such as stateful, concurrent, exceptional, hybrid, branching time, etc. We detach Kleene iteration from Kleene algebra and analyze it from the categorical perspective. The notion, we arrive at is that of Kleene-iteration category (with coproducts and tests), which we show to be general and robust in the sense of compatibility with programming language features, such as exceptions, store, concurrent behavior, etc. We attest the proposed notion w.r.t. various yardsticks, most importantly, by characterizing the free model as a certain category of (nondeterministic) rational trees.

In the monad-based approach to functional programming with effects, sequential composition, the primary high-level control structure for combining effectful functions, takes a special role. In this article, we advocate the idea that parallel composition should be recognized as a high-level control structure on an equal footing with sequential composition. We promote the concept of concurrent monad, which axiomatizes both sequential and parallel composition, and illustrate the approach by describing two concurrent monads for interleaving shared state concurrency: one of resumptions, the other of collections of traces.

Cellular automata are an archetypical comonadic notion of computation in that computation happens in the coKleisli category of a comonad. In this paper, we show that they can also be viewed as graded comonadic—a perspective that turns out to be both more informative and also more basic. We also discuss additive cellular automata to show that they admit both a graded comonadic and a graded monadic view. That these two perspectives are simultaneously available in this special case arises from a graded version of an observation by Kleiner about adjoint comonad-monad pairs.

Abstract Monad-comonad interaction laws are a mathematical concept for describing communication protocols between effectful computations and coeffectful environments in the paradigm where notions of effectful computation are modelled by monads and notions of coeffectful environment by comonads. We show that monad-comonad interaction laws are an instance of measuring maps from Sweedler theory for duoidal categories whereby the final interacting comonad for a monad and a residual monad arises as the Sweedler hom and the initial residual monad for a monad and an interacting comonad as the Sweedler copower. We then combine this with a (co)algebraic characterization of monad-comonad interaction laws to derive descriptions of the Sweedler hom and the Sweedler copower in terms of their coalgebras resp. algebras.

A large class of monads used to model computational effects have natural presentations by operations and equations, for example, the list monad can be presented by a constant and a binary operation subject to unitality and associativity. Graded monads are a generalization of monads that enable us to track quantitative information about the effects being modelled. Correspondingly, a large class of graded monads can be presented using an existing notion of graded presentation. However, the existing notion has some deficiencies, in particular many effects do not have natural graded presentations. We introduce a notion of flexibly graded presentation that does not suffer from these issues, and develop the associated theory. We show that every flexibly graded presentation induces a graded monad equipped with interpretations of the operations of the presentation, and that all graded monads satisfying a particular condition on colimits have a flexibly graded presentation. As part of this, we show that the usual algebra-preserving correspondence between presentations and a class of monads transfers to an algebra-preserving correspondence between flexibly graded presentations and a class of flexibly graded monads.

We introduce and study functor-functor and monad-comonad interaction laws as mathematical objects to describe interaction of effectful computations with behaviors of effect-performing machines. Monad-comonad interaction laws are monoid objects of the monoidal category of functor-functor interaction laws. We show that, for suitable generalizations of the concepts of dual and Sweedler dual, the greatest functor resp. monad interacting with a given functor or comonad is its dual while the greatest comonad interacting with a given monad is its Sweedler dual. We relate monad-comonad interaction laws to stateful runners. We show that functor-functor interaction laws are Chu spaces over the category of endofunctors taken with the Day convolution monoidal structure. Hasegawa's glueing endows the category of these Chu spaces with a monoidal structure whose monoid objects are monad-comonad interaction laws.

The Eilenberg-Kelly theorem states that a category C with an object I and two functors ⊗:C×C→C and ⊸:Cop×C→C related by an adjunction −⊗B⊣B⊸− natural in B is monoidal iff it is closed and moreover the adjunction holds internally. We dissect the proof of this theorem and observe that the necessity for a side condition on closedness arises because the standard definition of closed category is left-skew in regards to associativity. We analyze Street's observation that left-skew monoidality is equivalent to left-skew closedness and establish that monoidality is equivalent to closedness unconditionally under an adjusted definition of closedness that requires normal associativity. We also work out a definition of right-skew closedness equivalent to right-skew monoidality. We give examples of each type of structure; in particular, we look at the Kleisli category of a left-strong monad on a left-skew closed category and the Kleisli category of a lax closed monad on a right-skew closed category. We also view skew and normal monoidal and closed categories as special cases of skew and normal promonoidal categories and take a brief look at left-skew prounital-closed categories.

We discuss the relationship between monads and their known generalisation, graded monads, which are especially useful for modelling computational effects equipped with a form of sequential composition. Specifically, we ask if a graded monad can be extended to a monad, and when such a degrading is in some sense canonical. Our particular examples are the graded monads of lists and non-empty lists indexed by their lengths, which gives us a pretext to study the space of all (non-graded) monad structures on the list and non-empty list endofunctors. We show that, in both cases, there exist infinitely many monad structures. However, while there are at least two ways to complete the graded monad structure on length-indexed lists to a monad structure on the list endofunctor, such a completion for non-empty lists is unique.

The analysis of set comonads whose underlying functor is a container functor in terms of directed containers makes it a simple observation that any morphism between two such comonads factors through a third one by two comonad morphisms, whereof the first is identity on shapes and the second is identity on positions in every shape. This observation turns out to generalize into a much more involved result about comonad morphisms to comonads whose underlying functor preserves Cartesian natural transformations to itself on any category with finite limits. The bijection between comonad coalgebras and comonad morphisms from costate comonads thus also yields a decomposition of comonad coalgebras.

We provide syntactic derivative-like operations, defined by recursion on regular expressions, in the styles of both Brzozowski and Antimirov, for trace closures of regular languages. Just as the Brzozowski and Antimirov derivative operations for regular languages, these syntactic reordering derivative operations yield deterministic and nondeterministic automata respectively. But trace closures of regular languages are in general not regular, hence these automata cannot generally be finite. Still, as we show, for star-connected expressions, the Antimirov and Brzozowski automata, suitably quotiented, are finite. We also define a refined version of the Antimirov reordering derivative operation where parts-of-derivatives (states of the automaton) are nonempty lists of regular expressions rather than single regular expressions. We define the uniform scattering rank of a language and show that, for a regexp whose language has finite uniform scattering rank, the truncation of the (generally infinite) refined Antimirov automaton, obtained by removing long states, is finite without any quotienting, but still accepts the trace closure. We also show that star-connected languages have finite uniform scattering rank.

The delay datatype was introduced by Capretta (Logical Methods in Computer Science, 1(2), article 1, 2005) as a means to deal with partial functions (as in computability theory) in Martin-Löf type theory. The delay datatype is a monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay datatype quotiented by weak bisimilarity is still a monad–a constructive alternative to the maybe monad. In this paper, we consider the alternative approach of Hofmann (Extensional Constructs in Intensional Type Theory, Springer, London, 1997) of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. With the aid of these principles, we also prove that the quotiented delay datatype delivers free ω-complete pointed partial orders (ωcppos). Altenkirch et al. (Lecture Notes in Computer Science, vol. 10203, Springer, Heidelberg, 534–549, 2017) demonstrated that, in homotopy type theory, a certain higher inductive–inductive type is the free ωcppo on a type X essentially by definition; this allowed them to obtain a monad of free ωcppos without recourse to a choice principle. We notice that, by a similar construction, a simpler ordinary higher inductive type gives the free countably complete join semilattice on the unit type 1. This type suffices for constructing a monad, which is isomorphic to the one of Altenkirch et al. We have fully formalized our results in the Agda dependently typed programming language.

We introduce a method to lift monads on the base category of a fibration to its total category. This method, which we call codensity lifting, is applicable to various fibrations which were not supported by its precursor, categorical TT-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended pseudometric spaces to the category of sets, and also the fibration from the category of binary relations between measurable spaces. We also introduce the dual method called density lifting of comonads. We next study the liftings of algebraic operations to the codensity liftings of monads. We also give a characterisation of the class of liftings of monads along posetal fibrations with fibred small meets as a limit of a certain large diagram.

Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication usually called ‘exclusion’. A standard-style sequent calculus for this logic is easily obtained by extending multiple-conclusion sequent calculus for intuitionistic logic with exclusion rules dual to the implication rules (in particular, the exclusion-left rule restricts the premise to be single-assumption). However, similarly to standard-style sequent calculi for non-classical logics like S5, this calculus is incomplete without the cut rule. Motivated by the problem of proof search for propositional bi-intuitionistic logic (BiInt), various cut-free calculi with extended sequents have been proposed, including (i) a calculus of nested sequents by Goré et al., which includes rules for creation and removal of nests (called ‘nest rules’, resp. ‘unnest rules’) and (ii) a calculus of labelled sequents by the authors, derived from the Kripke semantics of BiInt, which includes ‘monotonicity rules’ to propagate truth/falsehood between accessible worlds. In this paper, we develop a proof-theoretic study of these three sequent calculi for BiInt grounded on translations between them. We start by establishing the basic meta-theory of the labelled calculus (including cut-admissibility), and use then the translations to obtain results for the other two calculi. The translation of the nested calculus into the standard-style calculus explains how the unnest rules encapsulate cuts. The translations between the labelled and the nested calculi reveal the two formats to be very close, despite the former incorporating semantic elements, and the latter being syntax-driven. Indeed, we single out (i) a labelled calculus whose sequents have a ‘label in focus’ and which includes ‘refocusing rules’ and (ii) a nested calculus with monotonicity and refocusing rules, and prove these two calculi to be isomorphic (in a bijection both at the level of sequents and at the level of derivations).

Abstract Rational sequences are possibly infinite sequences with a finite number of distinct suffixes. In this paper, we present different implementations of rational sequences in Martin–Löf type theory. First, we literally translate the above definition of rational sequence into the language of type theory, i.e., we construct predicates on possibly infinite sequences expressing the finiteness of the set of suffixes. In type theory, there exist several inequivalent notions of finiteness. We consider two of them, listability and Noetherianness, and show that in the implementation of rational sequences the two notions are interchangeable. Then we introduce the type of lists with backpointers, which is an inductive implementation of rational sequences. Lists with backpointers can be unwound into rational sequences, and rational sequences can be truncated into lists with backpointers. As an example, we see how to convert the fractional representation of a rational number into its decimal representation and vice versa.

Effects and coeffects are two general, complementary aspects of program behaviour. They roughly correspond to computations which change the execution context (effects) versus computations which make demands on the context (coeffects). Effectful features include partiality, non-determinism, input-output, state, and exceptions. Coeffectful features include resource demands, variable access, notions of linearity, and data input requirements. The effectful or coeffectful behaviour of a program can be captured and described via type-based analyses, with fine grained information provided by monoidal effect annotations and semiring coeffects. Various recent work has proposed models for such typed calculi in terms of graded (strong) monads for effects and graded (monoidal) comonads for coeffects. Effects and coeffects have been studied separately so far, but in practice many computations are both effectful and coeffectful, e.g., possibly throwing exceptions but with resource requirements. To remedy this, we introduce a new general calculus with a combined effect-coeffect system. This can describe both the changes and requirements that a program has on its context, as well as interactions between these effectful and coeffectful features of computation. The effect-coeffect system has a denotational model in terms of effect-graded monads and coeffect-graded comonads where interaction is expressed via the novel concept of graded distributive laws. This graded semantics unifies the syntactic type theory with the denotational model. We show that our calculus can be instantiated to describe in a natural way various different kinds of interaction between a program and its evaluation context.

Every context-free grammar can be transformed into an equivalent one in the Chomsky normal form by a sequence of four transformations. In this work on formalization of language theory, we prove formally in the Agda dependently typed programming language that each of these transformations is correct in the sense of making progress toward normality and preserving the language of the given grammar. Also, we show that the right sequence of these transformations leads to a grammar in the Chomsky normal form (since each next transformation preserves the normality properties established by the previous ones) that accepts the same language as the given grammar. As we work in a constructive setting, soundness and completeness proofs are functions converting between parse trees in the normalized and original grammars.

This special issue of Fundamenta

We show that a wide class of bidirectional data-flow analyses and program optimizations based on them admit declarative descriptions in the form of type systems. The salient feature is a clear separation between what constitutes a valid analysis and how the strongest one can be computed (via the type checking versus principal type inference distinction). The approach also facilitates elegant relational semantic soundness definitions and proofs for analyses and optimizations, with an application to mechanical transformation of program proofs, useful in proof-carrying code. Unidirectional forward and backward analyses are covered as special cases; the technicalities in the general bidirectional case arise from more subtle notions of valid and principal types. To demonstrate the viability of the approach we consider two examples that are inherently bidirectional: type inference (seen as a data-flow problem) for a structured language where the type of a variable may change over a program's run and the analysis underlying a stack usage optimization for a stack-based low-level language.

We present a new, semantics-based approach to mechanical program repair where the intended meaning of broken programs (i.e., programs that may abort under a given, error-admitting language semantics) can be defined by a special, error-compensating semantics. Program repair can then become a compile-time, mechanical program transformation based on a program analysis. It turns a given program into one whose evaluations under the error-admitting semantics agree with those of the given program under the error-compensating semantics. We present the analysis and transformation as a type system with a transformation component, following the type-systematic approach to program optimization from our earlier work. The type-systematic method allows for simple soundness proofs of the repairs, based on a relational interpretation of the type system, as well as mechanical transformability of program correctness proofs between the Hoare logics for the error-compensating and error-admitting semantics. We first demonstrate our approach on the repair of file-handling programs with missing or superfluous open and close statements. Our framework shows that this repair is strikingly similar to partial redundancy elimination optimization commonly used by compilers. In a second example, we demonstrate the repair of programs operating a queue that can over- and underflow, including mechanical transformation of program correctness proofs.

This special issue of the Journal of Functional Programming collects revised selected articles arising from the inaugural meeting of the Workshop on Mathematically Structured Functional Programming, MSFP 2006, held in Kuressaare, Estonia, on 2 July 2006, with support from the European Union's FP6 IST Coordination Action TYPES. This workshop raised the curtain for the Eighth International Conference on Mathematics of Program Construction, MPC 2006, but where MPC is concerned primarily with extrinsic mathematics supporting the programming process, MSFP has a complementary focus on the mathematics intrinsic to programs themselves. MSFP is about the extraction of functionality from structure.

Partial redundancy elimination is a subtle optimization which performs common subexpression elimination and expression motion at the same time. In this paper, we use it as an example to promote and demonstrate the scalability of the technology of proof optimization. By this we mean automatic transformation of a given program's Hoare logic proof of functional correctness or resource usage into one of the optimized program, guided by a type-derivation representation of the result of the underlying dataflow analyses. A proof optimizer is a useful tool for the producer's side in a natural proof-carrying code scenario where programs are proved correct prior to optimizing compilation before transmission to the consumer.

Data-flow analyses, such as live variables analysis, available expressions analysis etc., are usefully specifiable as type systems. These are sound and, in the case of distributive analysis frameworks, complete wrt. appropriate natural semantics on abstract properties. Applications include certification of analyses and "optimization" of functional correctness proofs alongside programs. On the example of live variables analysis, we show that analysis type systems are applied versions of more foundational Hoare logics describing either the same abstract property semantics as the type system (liveness states) or a more concrete natural semantics on transition traces of a suitable kind (future defs and uses). The rules of the type system are derivable in the Hoare logic for the abstract property semantics and those in turn in the Hoare logic for the transition trace semantics. This reduction of the burden of trusting the certification vehicle can be compared to foundational proof-carrying code, where general-purpose program logics are preferred to special-purpose type systems and universal logic to program logics. We also look at conditional liveness analysis to see that the same foundational development is also possible for conditional data-flow analyses proceeding from type systems for combined "standard state and abstract property" semantics.

Monads are commonplace programming devices that are used to uniformly structure computations with effects such as state, exceptions, and I/O. This paper further develops the monadic programming paradigm by investigating the extent to which monadic computations can be optimised by using generalisations of short cut fusion to eliminate monadic structures whose sole purpose is to "glue together" monadic program components.We make several contributions. First, we show that every inductive type has an associated build combinator and an associated short cut fusion rule. Second, we introduce the notion of an inductive monad to describe those monads that give rise to inductive types, and we give examples of such monads which are widely used in functional programming. Third, we generalise the standard augment combinators and cata/augment fusion rules for algebraic data types to types induced by inductive monads. This allows us to give the first cata/augment rules for some common data types, such as rose trees. Fourth, we demonstrate the practical applicability of our generalisations by providing Haskell implementations for all concepts and examples in the paper. Finally, we offer deep theoretical insights by showing that the augment combinators are monadic in nature, and thus that our cata/build and cata/augment rules are arguably the best generally applicable fusion rules obtainable.

This paper introduces $\lambda^\widehat$ , a simply typed lambda calculus supporting inductive types and recursive function definitions with termination ensured by types. The system is shown to enjoy subject reduction, strong normalisation of typable terms and to be stronger than a related system $\lambda_{\mathcal{G}}$ in which termination is ensured by a syntactic guard condition. The system can, at will, be extended to support coinductive types and corecursive function definitions also.

We investigate CPS translatability of typed λ-calculi with inductive and coinductive types. We show that tenable Plotkin-style call-by-name CPS translations exist for simply typed λ-calculi with a natural number type and stream types and, more generally, with arbitrary positive inductive and coinductive types. These translations also work in the presence of control operators and generalize for dependently typed calculi where case-like eliminations are only allowed in non-dependent forms. No translation is possible along the same lines for small Σ-types and sum types with dependent case.