[Aldor-l] Aldor-Meet

[Bill Page]

On 11/20/07, Jacques Carette wrote:
> Bill Page wrote:
> > In general I would not simply accept any as the "authority". I think
> > that would lead to the kind of subjective idiosyncrasies that we see
> > in most other languages. Rather I would very much rather that the
> > language be based on some commonly accepted theory - the more general
> > the better (e.g. category theory :-).
> In which case I would argue that Meet should be either some kind of
> pullback or (co)cone in the category of theories and theory morphism
> over an appropriate logic.

I am uneasy about the level of abstraction in your proposal. I think
one difficulty of applying category theory in a concrete manner to
programming languages is to convert such abstract specifications to
operational definitions. However I do agree that at a fundamental
level one should be concerned about an appropriate choice of logic.
Naively one might expect to deal with this by the usual definition of
Boolean in the Aldor language and library.  I think there are some
possible subtleties to worry about but maybe we can deal with this
later.

>
> See any of:
> 1) Bart Jacob's book "Categorical Logic and Type Theory",
> http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html
> 2) Jose Fiadeiro's book "Categories for Software Engineering"
> http://www.fiadeiro.org/jose/CATBook/
> 3) Joseph Goguen's "Types as theories"
> http://portal.acm.org/citation.cfm?id=135134
> 4) Tom Maibaum's "Theories as Types",
> de Queiroz R J G B, Maibaum, T S E, "Abstract Data Types and Type
> Theory: Theories as Types" Zeitschrift fur Mathematische Logik und
> Grundlagen der Mathematik, Vol 37, (1991), 149-166.
>
> along these lines,
> 5) Zhaohui Luo's "A higher order calculus and theory abstraction" is
> also relevant, http://portal.acm.org/citation.cfm?id=106148.106154
>

Thank you. All of these are very good references. But for example in
Joseph Goguen's oft quoted articel "Types as theories"
http://citeseer.ist.psu.edu/503432.html ( available at:
http://www.cse.ucsd.edu/users/goguen/projs/sem.html ) , I see a
concern with abstract concepts (e.g. category of theories) that do not
map immediately to concepts in Aldor. Of course I do not mean to imply
that they may not be operationalized in some other language (e.g. OBJ)
but only that I do not see these ideas immediately reflected in the
design of Aldor as it exists today. In particular Aldor (like Axiom)
has no built-in notion of how to represent axioms as such, so concepts
like equational theories can at best only be treated in the libraries.
Maybe "Types as Theories" might be applied as a principle of library
design but I have a hard time seeing it directly applied to the Aldor
language.

When I think of category theory in the context of Aldor I think of the
proposal Saul Youssef presented at the 2001 Aldor workshop:

  http://atlas.bu.edu/~youssef/papers/math/aldor/aldor.pdf

Saul mentioned this paper here recently in another context.
Specifically in that paper he wrote:

-- quote --

Consider an Aldor category with no signatures

  Domain:Category == with

Let objects in the mathematical sense be Aldor domains satisfying
Domain. If A and B are such domains, let Hom(A,B) be the collection of
Aldor functions with signature A -> B. Let the composition of f: A ->
B and g:B -> C be the Aldor function

  (a:A):C +-> g f a

and let the identity morphism of an object A be the Aldor function

  (a:A):A +-> a

we claim that this is, in fact, a category. Although we have no proof,
we are confident of this claim because of expected properties of Aldor
functions and Domains. We expect, for instance, that composition of
Aldor functions is associative. This suggests that

  o PreAxiom: Domain is a category.

be taken as part of our "model of computation". In more detail, we expect

  o Axiom: Domain is a category with finite products, coproducts,
initial, final and exponential objects.

based on expected properties of the Aldor functions, "Record" and
"Union" types. If Axiom is sufficient for rigorous arguments, it would
be especially satisfying since the definition of a category could
serve as the foundation for "regular" mathematics[1] and the existence
of a particular such category could serve as the foundation for
computation.

-- end quote --

The category named Domain in the quote above is the top of the Aldor
category subtype lattice and both Join and Meet are presumed to
operate on this lattice which is closed under these operations. But
all of these categories already come with a lot of structure
essentially already built-in the Aldor language. In fact, add just one
more operation (equality) and assume one more built-in object
(Boolean) and we have already have algebraic Sets (topoi). So I do not
think we can demand much more of the Join and Meet category
constructors in Aldor than that they obey the axioms of a (bounded)
lattice - commutativity, associativity and absorption:

  Join(A,Meet(A,B)) = Meet(A,Join(A,B)) = A

I think that reducing (evaluating) category expressions in this manner
should not be too demanding of the Aldor compiler and these could be
made to play nicely with the run-time operation 'has' of testing type
satisfaction.

> But of course pushouts (called Join in Aldor) have much clearer use
> cases.   In the  "little theories" approach,  which  the  designers of
> Axiom/Aldor seemed that have intuitively rediscovered (but never
> properly formalized),  most Categories and Domains would be done via
> Joins and other means of assembly from smaller pieces.
>

I would like to hear more about how Join in Aldor can be seen as a
pushout. I am concerned particularly about the treatment of Domains.
Are domains objects in some category as in Saul's definition above? Or
do we need to resort to a more abstract definition? Do we need to add
to Aldor some formal method of representing equational axioms? Etc.

Regards,
Bill Page.