This paper gives two new categorical characterisations of lenses: one as a coalgebra of the store comonad, and the other as a monoidal natural transformation on a category of a certain class of coalgebras. The store comonad of the first characterisat
ion can be generalized to a Cartesian store comonad, and the coalgebras of this Cartesian store comonad turn out to be exactly the Biplates of the Uniplate generic programming library. On the other hand, the monoidal natural transformations on functors can be generalized to work on a category of more specific coalgebras. This generalization turns out to be the type of compos from the Compos generic programming library. A theorem, originally conjectured by van Laarhoven, proves that these two generalizations are isomorphic, thus the core data types of the Uniplate and Compos libraries supporting generic program on single recursive types are the same. Both the Uniplate and Compos libraries generalize this core functionality to support mutually recursive types in different ways. This paper proposes a third extension to support mutually recursive data types that is as powerful as Compos and as easy to use as Uniplate. This proposal, called Multiplate, only requires rank 3 polymorphism in addition to the normal type class mechanism of Haskell.
Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively by dependent type theory and classical reasoning is typically supported
by adding additional non-constructive axioms. However, there is another perspective that views constructive logic as an extension of classical logic. This paper will illustrate how classical reasoning can be supported in a practical manner inside dependent type theory without additional axioms. We will see several examples of how classical results can be applied to constructive mathematics. Finally, we will see how to extend this perspective from logic to mathematics by representing classical function spaces using a weak value monad.
There are two incompatible Coq libraries that have a theory of the real numbers; the Coq standard library gives an axiomatic treatment of classical real numbers, while the CoRN library from Nijmegen defines constructively valid real numbers. Unfortun
ately, this means results about one structure cannot easily be used in the other structure. We present a way interfacing these two libraries by showing that their real number structures are isomorphic assuming the classical axioms already present in the standard library reals. This allows us to use OConnors decision procedure for solving ground inequalities present in CoRN to solve inequalities about the reals from the Coq standard library, and it allows theorems from the Coq standard library to apply to problem about the CoRN reals.
Compact sets in constructive mathematics capture our intuition of what computable subsets of the plane (or any other complete metric space) ought to be. A good representation of compact sets provides an efficient means of creating and displaying imag
es with a computer. In this paper, I build upon existing work about complete metric spaces to define compact sets as the completion of the space of finite sets under the Hausdorff metric. This definition allowed me to quickly develop a computer verified theory of compact sets. I applied this theory to compute provably correct plots of uniformly continuous functions.
Reasoning about real number expressions in a proof assistant is challenging. Several problems in theorem proving can be solved by using exact real number computation. I have implemented a library for reasoning and computing with complete metric space
s in the Coq proof assistant and used this library to build a constructive real number implementation including elementary real number functions and proofs of correctness. Using this library, I have created a tactic that automatically proves strict inequalities over closed elementary real number expressions by computation.
