[FOM] The FOM of objects and classes in programming languages
Patrik Eklund
peklund at cs.umu.se
Fri Mar 31 02:48:43 EDT 2017
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
More information about the FOM
mailing list