David,
I would like to recall something that you wrote on Thu, Apr 3, 2008 at 1:33 PM (in part):
I think that a far more fundamental question is "what is the relationship between the object- and the meta-language?" In this
case the meta-language is Aldor in which we express ideas and
algorithms about mathematics of interest.
As category theory is very expressive it is tempting to view all mathematics as applied category theory and say that the objects that we want to talk about: rings, Lie algebras, etc., are categories. That would make category theory the object
language. This doesn't necessarily imply anything about the meta-language, except that it ought to be able to manipulate the things of the object language easily.
...
Translated back into Aldor, the category theoretic constructions
that we want to talk about need not necessarily be the category
theoretic constructs that we want to use to talk about category theory.
------
I think you are absolutely correct to raise this issue. Why indeed should we attempt to design a language like Aldor at all? Afterall, in the final analysis all programming languages are essentially equally expressive - they all are (in principle) Turing-complete. So there is nothing we can do in one that we cannot (in principle) do in another.
I think the answer has to do with the expressiveness of the language. That is, how efficiently can we express the ideas (programs) that we need to express? It seems very likely to me that the most efficient language for this purpose is the metalanguage itself (otherwise it seems likely that if a more expressive language existed, mathematics would quickly adopt it).
So the closer our object language is to our metalanguage, the more "expressive" it is. It seems that the only thing that might prevent us from achieving this optimum is that the meta-language is not in general be entirely computable (or else it is in some essential respect inconsistent).
But category theory itself appears to have some kind of universal applicability. So I wonder if you would agree that in spite of having "translated back into Aldor" as you said above, that we can (and should) remain in category in so much as the formal semantics of Aldor can be specified in categorical terms?
I wonder however exactly what cateogory theory is most appropriate to describe such a programming language? One possible answer I think is topos theory - or by another name: algebraic set theory. Choosing this as the basis for the underlying semantics of the Aldor language would have numerous implications.
Bill.
