[FOM] The FOM of objects and classes in programming languages

[Patrik Eklund]

It's hard to fully understand objects and classes as they appear in 
programming languages if we only read about algebraic theories without 
using the language of category theory.

The algebraic (and coalgebraic) side of objects and classes, can be seen 
starting from Lawvere's 1963 paper, and an example of a fairly good 
description to algebraic theories as supporting the understanding of the 
categorical structures to this is the algebraic theories by Adamek at 
al:

http://www.iti.cs.tu-bs.de/~adamek/algebraic.theories.pdf

The programming language side is well explained in the Ehrig and Mahr 
foundations of algebraic specifications:

http://www.springer.com/la/book/9783642699641
https://link.springer.com/book/10.1007%2F978-3-642-61284-8

Then there are obviously new books and papers "explaining" various 
situations but they mostly depart from the FOM aspects of objects.

---

One tricky part is related to types (sorts in the underlying signature), 
and in particular to type constructors, as that is the place where 
computer science departs from mathematical treatments. Type constructors 
are usually brought in from the outside, so as to say. The 
interpretation of types, terms and substitutions is treated differently 
in respective programming languages.

Type constructors go back at least to Church 1940, and has thereafter 
never actually been treated properly. Church didn't go into types, and 
Curry didn't go into computation, so there was never really a curiosity 
about the interactions between types and computations.

Type constructors are operators and should reside in a signature kind of 
"over" the underlying signature, as we have explained some years ago 
(http://www.glioc.com/files_glioc/ModernEyesOnLambdaCalculus.pdf). This 
opens the difficult question about models. Let me take just one example. 
If nat is the type for numbers in the "Peano signature", and for some 
reason we need to build the powertype. Then we need to say that nat is a 
constant in a new signature with the sort 'type', so that "nat : -> 
type" is a constant in that new signature "over" the Peano signature. 
Then we could introduce the powertype constructor like "P : type -> 
type" to so that Pnat is a new and constructed type. The hard part now 
is the algebra of 'type', and it is not just an algebra, but something 
beyond. We believe it must be something like the object set of a 
monoidal closed category, so that the model of type constructors are 
functors. Needless to say, in universal algebra we have "free" e.g. like 
in a free monoid, but for monoidal categories we don't have "free 
monoidal categories".

Computer Science needs help with these things and I think some extension 
and generalization of universal algebra is needed, and FOM machineries 
will certainly come into play. We do not know how, but we will, as 
Hilbert said (Wir müssen wissen! Wir werden wissen!). However, computer 
scientists are reluctant to think in these terms, and mathematicians and 
foundationalists seem not bring this into their research agendas.

The slogan here could be that "Aristotle is without types, and Plato is 
full of it".

Obviously, the thoughts concerning types and powers of at least a few 
within the FOM community go to Principia Mathematica, and that's ok, but 
for elaborate computations we need more elaborate type constructors than 
just the powertype constructor.

---

Good news is that the intermediate languages are coming closer to each 
other since the giants producing these intermediate languages act in 
common working groups. This means that the intermediate languages like 
those for Java and C are now closer to Microsoft's .NET languages like 
C# and F#. These intermediate languages are indeed languages to which 
programming languages compile, and from which the compiled source code 
translates to machine language. This obviously means that an object or a 
class translates to such an intermediate language and further on to 
machine. FOM is more relevant in the first translation, since in the 
latter translation, math and logic is mostly left in the gutter. The 
notion of 'variable' and 'substitution' is treated differently in 
languages. Substitution is the morphism in the Kleisli category over the 
term monad based on the underlying signature (sorts and operations) for 
the language. Kleisli morphisms are substitutions.

Concerning .NET we may note that Microsoft Research in Cambridge has 
been dealing with these issues to some extent, but unfortunately not all 
that deeply. It shows e.g. in categorical ingredients in Haskell and how 
Haskell still hasn't been able to close the deal about foundational 
issues.

---

Not to be critical at all, but my impression of FOM is that it is often 
happily hindsighted and even eager to write and rewrite history of FOM, 
but less foresighted to produce and provide new tools to help solve 
problems where obviously FOM ingredients appear, like in the situation 
concerning "object".

---

Best,

Patrik