Diagram Combinators in MMT

摘要

Formal libraries, especially large ones, usually employ modularity to build and maintain large theories efficiently. Although the techniques used to achieve modularity vary between systems, most of them can be understood as operations in the category of theories and theory morphisms. This yields a representation of libraries as diagrams in this category, with all theory-forming operations extending the diagram. However, as libraries grow even bigger, it. is starting to become important to build these diagrams modularly as well, i.e., we need languages and tools that support computing entire diagrams at once. A simple example would be to systematically apply the same operation to all theories in a diagram and return both the new diagram and the morphisms that relate the old one to the new one. In this work, we introduce such diagram combinators as an extension to the MMT language and tool. We provide many important combi-nators, and our extension allows library developers to define arbitrary new ones. We evaluate our framework by building a library of algebraic theories in an extremely compact way.