Vector bases, arrays, and adjunctions
Jonathon Burns – 4 March 1998
What does it mean for Cartesian coordinate systems to be first-class objects in programming languages? Investigation leads to a derivation of tensor algebra as an additive category which is also Cartesian closed. Along the way, we encounter: exponentials with special structure, in this case the biproduct; an application of the isomorphism defined by two functors right-adjoint to a single left-adjoint; and a very general conception of programming languages, as term-rewriting or reduction policies on equational theories defined by adjunctions.