ABSTRACT. Polynomials (also known as containers) represent datatypes which, like polynomial functions, can be expressed using sums and products. Extending this analogy, I will describe the category of polynomials in terms of sums and products for fibrations. This category arises from a distributive law between the pseudomonad ‘freely adding’ indexed sums to a fibration, and its dual adding indexed products. A fibration with sums and products is essentially the structure defining a categorical model of dependent type theory. I will show how the process of adding sums to such a fibration is an instance of a general 'gluing' construction for building new models from old ones. In particular we can obtain new models of type theory in categories of polynomials. Finally, I will explore the properties of other type formers in these models, and consider which logical principles are and are not preserved by the construction.

ABSTRACT. While papers showing examples of distributive laws are abundant, papers containing the opposite result - that certain distributive laws cannot exist - are rarely seen. In fact, the only example known to us is in 'Distributing Probability over Nondeterminism' by Varacca and Winskel, which contains a proof by Plotkin that the probability monad does not distribute over the powerset monad. In 2008, Manes and Mulry posed the question of whether the list monad distributes over itself. We solve this question, proving that both the list monad and powerset monad do not distribute over themselves, while there is precisely one distributive law for the multiset monad over itself.

ABSTRACT. In this paper a constructive formalization of quantifier elimination is presented, based on a classical formalization by Tobias Nipkow (2008, "Reflecting Quantifier Elimination for Linear Arithmetic"). The formalization is implemented and verified in the programming language/proof assistant Agda. It is shown that, as in the classical case, the ability to eliminate a single existential quantifier may be generalized to full quantifier elimination and consequently a decision procedure. The latter is shown to have strong properties under a constructive metatheory, such as the generation of witnesses and counterexamples. Finally, this is demonstrated on a minimal theory on the natural numbers.

ABSTRACT. We revisit once again the connection between three notions of computation: monads, arrows and idioms (also called applicative functors). We employ monoidal categories of finitary functors and profunctors on finite sets as models of these notions of computation, and develop the connections between them through adjunctions. As a result, we obtain a categorical version of Lindley, Yallop and Wadler’s characterisation of monads and idioms as arrows satisfying an isomorphism.

ABSTRACT. Ornaments have been introduced as a means to lift functions operating on some datatype into new functions operating on an ornamentation of this datatype, i.e., a variant of this datatype carrying additional information. A typical example consists in viewing lists as an ornamentation of natural numbers and then lifting the addition into the concatenation---the user just providing the missing parts of the code. Ornaments have first been introduced in Agda and extensively studied in a categorical setting.

We have been exploiting and adapting the idea of ornamentation in the context of ML. Here, we are interested in syntactic liftings where the lifted function is related to the original one as in the general setting but with a closer correspondence: on the one hand, the behavior (and ideally the computation steps) of the lifted function should coincide with the behavior of the original function, except for the additional user-provided code; on the other hand, the lifted code should be as close as possible to the code the user would have manually written.

Our approach is to first synthesize a generic version of the base program that can then be specialized to any ornamentation of the base version (including the base version as a particular case), and finally simplified. While the generic version of ML base code requires some form of dependent types to typecheck, we ensure by construction, using staged computation and dependent types, that each instantiation to concrete ornaments can be simplified back into ML code.

We use parametricity to show the correspondence between the base and lifted versions. We verified on (small) examples that the lifted code is often close to hand-written code.

This approach to ornamentation can be extended to perform disornamentation---with new design challenges and interesting applications. Ornamentation and disornamentation are just two examples of a more general type-based approach to code refactoring and evolution.

ABSTRACT. Profunctor optics are a neat and composable representation of bidirectional data accessors, including lenses, and their dual, prisms. The profunctor representation exploits higher-order functions and higher-kinded type constructor classes. The relationship between the profunctor representation and the familiar representation in terms of "getter" and "setter" functions is not at all obvious. We derive the former from the latter, making the relationship clear. It turns out to be a fairly direct application of the Yoneda Lemma, arguably the most important result in category theory.

ABSTRACT. We present a method of backward induction for computing approximate subgame perfect Nash equilibria of infinitely repeated games with discounted payoffs. This uses the selection monad transformer, combined with the searchable set monad viewed as a notion of 'topologically compact' nondeterminism, and a simple model of computable real numbers. This is the first application of Escardó and Oliva's theory of higher-order sequential games to games of imperfect information, in which (as well as its mathematically elegance) lazy evaluation does nontrivial work for us compared with a traditional game-theoretic analysis. Since a full theoretical understanding of this method is lacking (and appears to be very hard), we consider this an 'experimental' paper heavily inspired by theoretical ideas. We use the famous Iterated Prisoner's Dilemma as a worked example.

ABSTRACT. This literate Agda paper gives a nameless co-de-Bruijn representation of generic (meta)syntax with binding. It owes much to the work of Sato et al. on representation of variable binding by mapping variable use sites. The key to any nameless representation of syntax is how it indicates the variables we choose to use and thus, implicitly those we neglect. The business of selecting is what we shall revisit with care, ensuring that all free variables are used. The definition leads to a new, structurally recursive, construction of simultaneous hereditary substitution, given generically for a universe of syntaxes with metavariables.