Category Theory

A Topos Foundation for Theories of Physics

A Topos Foundation for Theories of Physics: I. Formal Languages for Physics. Andreas Döring and Chris Isham.

This paper is the first in a series whose goal is to develop a fundamentally new way of constructing theories of physics. The motivation comes from a desire to address certain deep issues that arise when contemplating quantum theories of space and time. Our basic contention is that constructing a theory of physics is equivalent to finding a representation in a topos of a certain formal language that is attached to the system. Classical physics arises when the topos is the category of sets. Other types of theory employ a different topos. In this paper we discuss two different types of language that can be attached to a system, S. The first is a propositional language, PL(S); the second is a higher-order, typed language L(S). Both languages provide deductive systems with an intuitionistic logic. The reason for introducing PL(S) is that, as shown in paper II of the series, it is the easiest way of understanding, and expanding on, the earlier work on topos theory and quantum physics. However, the main thrust of our programme utilises the more powerful language L(S) and its representation in an appropriate topos.

This is a little outside of our usual areas, but I think it will appeal to at least some readers. Personally, I find the approach aesthetically very, very appealing for several reasons, and I would be thrilled if an answer to quantum cosmology came from this direction, but I'm the first to admit that my grasp of the phsyics is barely enough to follow along. I was able to make it through this paper fairly easily, but things aren't too interesting in the classical case, and I sadly suspect that the application to quantum physics in parts II and III will leave me behind.

Via The n-Category Cafe, where there is also considerable discussion, much of it around the single word "peristalithic"...

Propositions as [Types]

Propositions as [Types], Steve Awodey and Adrej Bauer.

Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational content, and formalizing a notion of proof irrelevance. Indeed, semantically, the notion of a support is sometimes used as surrogate proposition asserting inhabitation of an indexed family.

We give rules for bracket types in dependent type theory and provide complete semantics using regular categories. We show that dependent type theory with the unit type, strong extensional equality types, strong dependent sums, and bracket types is the internal type theory of regular categories, in the same way that the usual dependent type theory with dependent sums and products is the internal type theory of locally cartesian closed categories.

We also show how to interpret first-order logic in type theory with brackets, and we make use of the translation to compare type theory with logic. Specifically, we show that the propositions-as-types interpretation is complete with respect to a certain fragment of intuitionistic first-order logic. As a consequence, a modified double-negation translation into type theory (without bracket types) is complete for all of classical first-order logic.

I figure I should say a few words about why proof irrelevance is an interesting idea. In math, you often want to consider elements of a certain type that have certain properties -- for example, you might want the set of satisfiable boolean formulas as part of a proof as a hypothesis of a theorem.

The way you might represent this in dependent type theory is by giving a pair, consisting of a formula and a satisfying assignment. You might write this as sigma f:Formula. assignment(f). The trouble is that the elements of this type really have more information than the subset contains; in addition to having formulas, you also have the assignments. So if you wanted to write a function that took values of this type computed satisfying assignments, then you could do it in constant time by just returning the second component of the pair, the evidence that it was satisfiable. This is not what you want, if your goal was to show that you could compute the satisfying assignment to a satisfiable formula.

One way of addressing this problem is to treat the second component of the pair as a proof irrelevant type. The basic idea is that for each type A, you make up a new type [A] which has either zero or one inhabitants, depending on whether A has any inhabitants or not. This means that you cannot make any computational use of data of type [A], because it doesn't have any structure to it. So if your solver receives a value of type sigma f:Formula. [assignment(f)], then you know that the formula is satisfiable, but you don't know what it is, because the second component is a bracket type. This means that your function will actually have to do the real work you intended.

I should also add that this is an old idea in type theory; this is the paper that made it clear to me.

(Thanks to Bob Harper for suggesting clarifications to my comments.)

Using Category Theory to Design Implicit Conversions and Generic Operators

Using Category Theory to Design Implicit Conversions and Generic Operators, John C. Reynolds, 1980. (Try this if the official link doesn't work.)

A generalization of many-sorted algebras, called category-sorted algebras, is defined and applied to the language design problem of avoiding anomalies in the interaction of implicit conversions and generic operators. The definition of a simple imperative language (without any binding mechanisms) is used as an example.

This is an old, but still cute, paper. The basic intuition is that a good design principle for a language with implicit conversions is that whatever order of conversions the language takes, you should get the same result. He then formalizes that by giving a category of types and conversions, and demanding that everything commute properly. And these give just the conditions the language designer has to check to make sure that he or she hasn't screwed anything up.

Someone could probably get a fun little paper by taking this idea and shooting some dependent types into it. (Maybe somebody already has?) If you've got an abstract type, a coercion function, and a proof that it satisfies Reynolds' conditions, now your compiler can silently insert those coercions for you as needed, but you can still be sure that it won't mess up the meaning of your program.

Holodeck games and CCCs

From the n-Category Cafe, some notes on Holodeck Games and cartesian closed categories.

This also appeared here (and was mentioned by Phil Wadler). The two posts seem to have different addenda, comments and links, so it may be worth looking at both.

It's fun to see lambda calculus introduced to an audience already familiar with categories, as that seems to be the opposite of the usual state of affairs around here, and I can think of certain LtU regulars who will hopefully find this whole subject enjoyable.

Arrows, like Monads, are Monoids

By Chris Heunen and Bart Jacobs

At first, these Arrows may look somewhat arbitrary. Here we show that they are categorically fairly civilised, by showing that they correspond to monoids in suitable subcategories of bifunctors Cop × C → C. This shows that, at a suitable level of abstraction, arrows are like monads …

Folds, Church Encodings, Builds, and Short Cut Fusion for Nested Types: A Principled Approach

by Neil Ghani and Patricia Johann:

Initial algebra semantics is one of the cornerstones of the theory of modern programming languages. It provides support for fold combinators encapsulating structured recursion over data structures, thereby making it possible to both reason about and transform programs in principled ways. Recently, Ghani, Uustalu, and Vene extended the usual initial algebra semantics to support not only standard fold combinators for inductive types, but also Church encodings and build combinators for them. In addition to being theoretically useful in ensuring that build is seen as a fundamental part of the basic infrastructure for programming with inductive types, this development has practical merit: the fold and build combinators can be used to define fold/build rules which optimise modularly constructed programs by eliminating intermediate inductive data structures.

In this paper, we apply this extended initial algebra semantics to the theory and practice of programming with nested data types. In particular, we use it to simplify the theory of folds for nested types, as well as to provide the first Church encodings, build combinators, and fold/build fusion rules for them.

Code for "Folds, Church Encodings, Builds, and Short Cut Fusion for Nested Types: A Principled Approach"

Socially Responsive, Environmentally Friendly Logic

Socially Responsive, Environmentally Friendly Logic
by Samson Abramsky

We consider the following questions: What kind of logic has a natural semantics in
multi-player (rather than 2-player) games? How can we express branching quantifiers, and
other partial-information constructs, with a properly compositional syntax and semantics?
We develop a logic in answer to these questions, with a formal semantics based on multiple
concurrent strategies, formalized as closure operators on Kahn-Plotkin concrete domains.
Partial information constraints are represented as co-closure operators. We address the
syntactic issues by treating syntactic constituents, including quantifiers, as arrows in a
category, with arities and co-arities. This enables a fully compositional account of a wide
range of features in a multi-agent, concurrent setting, including IF-style quantifiers.

This paper seems to unify multiple interesting directions - logic, game semantics, concurrent constraint programming (and concurrent programming in general).

At the same time it remains very accessible, without overwhelming amount of math, so can be hopefully useful not only for academics. I, for one, was waiting for exactly this kind of paper for two years (and my interest is very practical).

Multiplayer Curry-Howard correspondence, anyone? Or Curry-Howard for web services?

When is one thing equal to some other thing?

For those of you still looking, here's a fun introduction to Category Theory by Barry Mazur.

The Haskell Programmer's Guide to the IO Monad --- Don't Panic

The Haskell Programmer's Guide to the IO Monad - Don't Panic. Stefan Klinger.

Why do I need a monad for IO in Haskell? The standard explanation is, that the IO monad hides the non-functional IO actions ---which do have side effects--- from the functional world of Haskell. But how does this "hiding" work, apart from having IO actions disappearing beyond the borders of my knowledge?

This report scratches the surface of category theory, an abstract branch of algebra, just deep enough to find the monad structure. On the way we discuss the relations to the purely functional programming language Haskell. Finally it should become clear how the IO monad keeps Haskell pure.

It's hard for me to judge how successful this tutorial is going to be with beginners, but it seems well written.

The target audience isn't porgrammers trying to learn about monads as a programming construct, but rather programmers that want to get a taste of theory.

Combining computational effects

While some researchers seek to generalize monads (to arrows), others try to narrow the focus to achieve a richer theory (and probably deeper understanding).

Combining computational effects: commutativity and sum

We begin to develop a unified account of modularity for computational effects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi's paradigm for modelling computational effects; we emphasise the importance here of the operations that induce computational effects. Effects qua theories are then combined by appropriate bifunctors (on the category of theories). We give a theory of the commutative combination of effects, which in particular yields Moggi's side-effects monad transformer (an application is the combination of side-effects with nondeterminism). And we give a theory for the sum of computational effects, which in particular yields Moggi's exceptions monad transformer (an application is the combination of exceptions with other effects).
A longer version: Combining Effects: Sum and Tensor
XML feed