The n-Category Café

I’m fascinated by how categories can be applied both to physics (where we can think of a morphism as a physical process and draw it as a Feynman diagram or a circuit diagram) and to computer science (where we can think of a morphism as a program that takes data of some type as input, and spits out data of some other type).

Clearly these two applications must meet somewhere when we try to implement programs as actual physical processes! But how, exactly?

Yesterday Dan Ghica gave a talk on ‘Applications of game semantics: from program analysis to hardware synthesis’. Unfortunately I missed that talk. But today he told me a bit about it. Among other things, he said that symmetric monoidal closed categories are a useful framework for the problem of converting programs written in a high-level language into hardware specifications.

The point is that hardware amounts to black boxes hooked up by wires, and that’s what symmetric monoidal closed categories are good for! An example is the category of ‘handshake circuits’ in Section 3 of his paper Geometry of synthesis: a structured approach to VLSI design.

The first section of his paper Function interface models for hardware compilation is also very interesting. For example:

The problem of synthesis of gate-level descriptions of digital circuits from behavioural specifications written in higher-level programming lan- guages (hardware compilation) has been studied for a long time yet a definitive solution has not been forthcoming. The argument of this essay is mainly methodological, bringing a perspective that is informed by recent developments in programming-language theory. We argue that one of the major obstacles in the way of hardware compilation becoming a useful and mature technology is the lack of a well defined function interface model, i.e. a canonical way in which functions communicate with arguments. We discuss the consequences of this problem and propose a solution based on new developments in programming language theory.

On the one hand, ‘type theory’, profoundly related to category theory, has been widely adopted in the analysis and design of high-level languages. He quotes Robert Harper on this:

Over the last two decades type theory has emerged as the central organizing framework for the design and implementation of programming languages. Type theory (the study of type systems) provides the theoretical foundation for safe component integration. In the words of John Reynolds, “a type system is a syntactic discipline for enforcing levels of abstraction”. By syntactic we mean that the type system is part of the program, rather than purely in the mind of the implementer. By discipline we mean that type restrictions are enforced; ill-typed combinations are ruled out by the type system. By levels of abstraction we mean the clean separation between conceptually distinct data objects that may, in a particular program or compiler, have the same or similar representations. Implicit in this definition is an important principle: the power of a type system lies as much in what it precludes as what it allows. The most powerful type system of all is the one that rules out all programs. However, such a type system, while surely preventing safety violations, is hardly very useful. The goal of type system design is to increase expressiveness by admitting useful programs, but without compromising safety.

Particularly crucial is the ability to talk about ‘function types’ — this is where the closedness in symmetric monoidal categories is important:

Function interface models

Functions and related concepts (procedures, methods, subroutines, etc.) are the main mechanism for implementing abstraction in a programming language. The importance of using functional abstractions lies at the core of any good programming methodology and its benefits have long been established.

All three initial major modern programming languages (Fortran, Lisp, Cobol) provided support for functions, albeit sometimes in a clumsy or limited way. Of the three, the most advanced support for functions is found in Lisp. Not only does it support higher-order functions (functions that take functions as arguments) but it also introduced the new concept of a Foreign Function Interface: a way for a program written in Lisp to call functions written in another programming language. This idea was adopted by all subsequent programming languages that had mature compilers, under one name or another…

He seems to use the term ‘function interface model’ (FIM) to mean a setup for dealing with all the above issues involving functions. I would be glad to think of the theory of symmetric monoidal closed categories as a very basic ‘function interface model’.

But on the other hand, it’s not obvious how all these abstract ideas play out at the level of hardware! The idea of ‘hardware compilation’ makes this problem more than merely theoretical. Nicklaus Wirth explains what ‘hardware compilation’ means:

Automatically translating a program specified in a programming language into a digital circuit is an idea of long-standing interest. Thus far, the concept has appeared to be an uneconomical method of largely academic, but hardly practical, interest. It has therefore not been pursued with vigor and consequently has remained an idealist’s dream. With the increasing use of hardware description languages, however, it has become evident that hardware and software design share several traits.

They have traits in common, but also big differences. Where in software we build big programs out of ‘subroutines’ or ‘functions’, in hardware we build big circuits out of so-called ‘modules’. Here a ‘module’ is a fancy name for what we might also call a ‘black box’, with some wires going in, and some wires going out. The interesting thing is how ‘modules’ are less flexible than ‘functions’. Dan Ghica explains:

FIMs and hardware compilation

It is taken as a given that stored-program computers must offer well-defined function interface models (FIMs). It is inconceivable to design a modern operating system or compiler if this fundamental requirement is not met. On the other hand, in the world of hardware the concept of a FIM simply did not arise. The net-lists (boxes and wires) that are the underlying computational models of hardware languages are not structured in a way that suggests any obvious native FIM.

The abstraction mechanism common in hardware languages such as Verilog or VHDL, the module, is a form of placing a design inside a conceptual box with a specified interface. This does serve the purpose of hiding the implementation details of the module from its user, which is one of the main advantages of abstraction. However, a module is a less powerful than functional abstraction as found in programming languages in several significant ways:

1. Modules are always first order. A module can only take data as input and not other modules; in contrast, functions can take other functions as input.

2. Modules must be explicitly instantiated. The hardware designer must manually keep track of the names of each module occurrence and its ports, which must be connected explicitly by wires to other elements of the design. In contrast, the run-time management of various instances of functions is managed by the OS (using activation records) in a way that is transparent to the programmer.

3. Sharing a module from various points in a design is not supported by hardware design languages. The designer must design ad hoc circuitry, such as multiplexers or de-multiplexers and ad hoc protocols to achieve this. The lack of language support for sharing makes this a delicate and error-prone task.

It would be nice to understand these difference between ‘modules’ and ‘functions’ in category-theoretic terms. I bet Dan Ghica already knows a lot about this, and probably there’s a lot more about it in his papers! But this is all I know right now.