Computable functions may be defined in terms of Turing machines or recursive functions, or some other model of computation. We normally say that the choice doesn't matter, because all models of computation are equivalent. However, something about this bothers me.
Turing machines, for example, operate on strings of tokens, taking strings as input and giving strings as output. If we have another model of computation that also operates on strings then we have no problem saying formally whether it's equivalent to a Turing machine. However, if our model of computation operates on something other than strings then we have to define a mapping from its inputs and outputs to strings, and it seems there is no way to formally define whether that mapping is computable or not. (If I am wrong about this, please correct me.) So whenever we talk about equivalence between Turing machines and some non-string based model of computation, we are invoking an informal step; this seems unsatisfying.
It occurs to me that category theory might offer a way out of this, and I'm wondering if this has been done. For example, suppose we define a category with one object, to be interpreted as the set of all strings on some alphabet. We draw an arrow from this set to itself for every (partial) function that can be computed with a Turing machine, and define composition of arrows as function composition.
It is clear that this forms a category. My question is whether this category by itself (i.e. just the morphisms and their relationships, without reference to the underlying string type) tells us everything we need to know about computable functions. In other words, would it make sense to define Turing equivalence in terms of isomorphism to this category?
What I have in mind here is something like this: suppose we're given a model of computation that computes partial functions from some set $S$ to itself. We can then form a category of all partial functions that can be computed by this system and check whether this category is isomorphic to the similar category for Turing machines as defined above. This is appealing, if it works, because we never needed to define a mapping between the elements of $S$ and the elements of the set of strings. (But I'm worried it might not work, due to the possibility of the category isomorphism itself being uncomputable, in some sense.)
Finally, if this idea doesn't work, is there some way to fix it so that it does? I would be interested to hear about any work on defining or reasoning about the set of computable partial functions from a purely categorical point of view, so that it can be characterised without reference to a particular underlying model of computation.
Best Answer
You are looking for realizability toposes and related categories, as was already pointed out in the comments. Let me make a quick summary of how things work and why we can completely circumvent the dilemmas involving arbitrary codings of objects with strings.
To understand what is going on we do not need realizability toposes, as these are quite technically involved. We can use the much simpler assemblies. First we fix a model of computation $A$. Formally, $A$ should be a partial combinatory algebra, but informally you can just imagine Turing machines, or programs in a general-purpose programming language. An assembly $(S, \Vdash_S)$ is a set $S$ together with a realizability relation ${\Vdash_S} \subseteq A \times S$. We read $p \Vdash_S x$ as "program $p$ is a code of element $x \in S$". We require that $\Vdash_S$ have the property $\forall x \in S . \exists p \in A . p \Vdash_S x$, i.e., every element has to have at least one code. (But the same code may be shared between elements.) The notion of an assembly is very natural and it precisely captures the idea the the elements of an abstract set are encoded in some way by programs.
A morphism of assemblies $f : (S, \Vdash_S) \to (T, \Vdash_T)$ is map $f : S \to T$ which is realized, by which we mean that there is a program $q \in A$ such that $$p \Vdash_S x \implies q \cdot p \Vdash_T f(x).$$ This again is a completely natural idea which captures precisely the fact that the program $q$ operates on codes the way $f$ operates on the corresponding elements. It is what programmers do when you ask them to implement a mathematical function.
The category of assemblies is not a topos, but it is good enough to allow interpretation of lots of constructions and of intuitionistic first-order logic. The interpretation is completely standard (predicates are interpreted as subobjects, and everything else follows from that).
Here is the punch line: take an object of interest, say the real numbers. Characterize the real numbers in the language of first-order logic (or higher-order logic if needed, but then we have to use the topos), for instance "the Cauchy-complete archimedean ordered field". Up to isomorphism there is at most one assembly which satisfies this characterization. Therefore, there is no question about how real numbers should be represented! As soon as we say precisely what structure we expect of the reals, the encoding is imposed by the ambient category of assemblies (or the topos).
This trick works over and over again. You can start with the natural numbers, for example take $\mathbb{N}$ to be the free algebra for the signature $(0, 1)$, i.e., the free structure with one constant and one unary operation. Since initial algebras are unique up to unique isomorphisms, the assembly of natural numbers is determined.
We can go on:
Eventually it gets a bit tricky, for instance $L^p[0,1]$ is doable for $p < \infty$, it is not really doable for $L^\infty[0,1]$ (because this space is intuitionistically problematic anyhow), and I don't know whether spaces of distributions have been handled properly. As a rule of thumb, anything that constructive mathematicians can do, you can interpret in realizaiblity to obtain a computable version.
So your hunch was correct: categorical logic (which is just model theory in categories instead of sets) and realizaibility provide the answer.