[Aldor-l] Aldor-Meet

[Jacques Carette]

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.

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

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.
 
Jacques