[Aldor-l] [open-axiom-devel] [#428] 'Domain' in 'SetCategory'?

[root]

>> | > | I think the way out of this mess was correctly identified by Stephen
>> | > | Watt in the description of Aldor when he wrote: (ibid.):
>> | > |
>> | > | "Each domain is itself a value belonging to the domain Type. Domains
>> | > | may additionally belong to some number of subtypes (of Type), known
>> | > | as categories."
>>> ...
>>> Nothing in the semantics specification (the quote above without the
>>> first sentence) requires Type to be a domain.
>
>> I agree.
>
>Yep.
>
>I have no proof of it, but in my understanding Type is the type of all 
>Aldor types including itself. Type lives conceptually above domains and 
>categories. Maybe 'Type' is comparable to 'the class of all classes' in 
>set theory (even if NBG



I think part of the struggle is the attempt to unify the ideas of
type theory with the ideas of category theory. Being able to do so
would be deeply interesting but I don't think there is a "correct"
way to do it in any theoretical sense. It seems more of a pragmatic
choice. 

>From a computational point of view, categories and domains are just
type objects. There is no obvious reason why categories could not
include methods, although the methods might be restricted to functors
from domain to domain, or predicates to test that domains which claim
to belong to the category actually do satisfy some tests (e.g. that
the domain exports the required signatures and has the required
properties, like commutativity). Types do not need to know properties
of categories or domains.

>From a mathematical point of view, Categories and domains can be
constructed without types, although to do so would end up with a very
different system than Axiom. The design decision to use types to
enforce the category/domain machinery is not a necessary design
choice, although it is rather convenient. Someone could describe type
theory using category theory but I haven't seen it.

So from a programming viewpoint, types certainly include categories
and domains (since they are objects with representation and methods).
>From a mathematical point of view, types are convenient but unnecessary
to support the category/domain hierarchy which can all be built with
things, arrows, and composition.

So, within Axiom's design, types include categories/domains but not
the other way around.

Ultimately it seems just a design decision based on expected behavior,
so that the interaction between the type theory and the category
theory aspects gives reasonable results.

Tim