[Aldor-l] Type equivalence of domains in Axiom and Aldor

[Christian Aistleitner]

Hello,

On Fri, 26 Oct 2007 02:10:43 +0200, Bill Page <bill.page at newsynthesis.org>  
wrote:

> [...] I would propose the following definition of type-equivalence
> of domains:
>
>   Def: Two domains P and Q are equivalent if and only if both domains  
> satisfy
>   exactly the same set of categories: (P has x) = (Q has x) for all  
> Category
>   expressions x *and* neither P nor Q has any explicit exports that are  
> not
>   provided by some named category.

Although it's trivial to see, I thought it might be good to explicitly say  
that this property can only be checked at runtime--due to Aldor's "extend".

If P and Q are type equivalent in the above sense, linking the code with a  
further library extending only P by another named category breaks type  
equivalence.

> Obviously it makes sense to require that two equivalent domains must
> provide the same set of exported operations (the same interface)
> having the same names and same signatures. But as I understand the
> intention of the semantics of categories in both Axiom and Aldor this
> is not enough. We want categories to represent abstract concepts
> usually with a well-defined mathematical meaning. That is the reason
> for explicitly referring to satisfaction of categories in the
> definition above. Further since domains can also explicitly include
> exported operations in the 'with' clause (i.e. "anonymous categories"
> as defined in the Aldor user's guide), if this mathematical meaning is
> carried only by the named categories, such anonymous categories must
> always be assumed to represent different categories in each domain in
> which they occur.

In a nutshell, you want each anonymous category to be different from any  
category.

My feeling about Aldor is different:
Important exports with well-defined semantics should be defined in named  
categories.
Unimportant exports, syntactic sugar and the like (so all the exports  
which do not represent some general mechanism and do not contribute to the  
essence of a domain) may go into unnamed categories.

Using such an intuition, unnamed categories and their current semantics  
for type satisfaction really fit the concept. Still, you could define type  
equivalence by just checking the named categories and ignoring the unnamed  
categories.

Currently, lots of domains do not stick to this intuition, but that's a  
different story.

> As a mininum it would probably be necessary to introduce two new
> cateogies: StreamCat(S) and ProductCat(X,Y). Then it would seem that
> would be necessary add code along the lines of
>
>    Product(A: SetCategory,B: SetCategory): ProductCat(A,B) with
>      if A has StreamCat(S) and B has StreamCat(S) then
>         StreamCat(S)
>
> And
>
>   Stream(S:Type): StreamCat(S) with
>     if S has ProductCat(A,B) then
>        ProductCat(A,B)
>
> for some set of allowed domains A, B and S, including for example
> 'Integer'. Of course there is a problem here about specifying the
> specific list of domains for A, B and C. It would be desirable I
> think, if the compiler could produce generic code which would apply
> whtn A, B and C are still unknowns.

The code seems to somehow model a distributive law you described above.  
That's ok for me, but I cannot see how this relates to type equivalence.
Assume, I give you a binary operator "type-equivalent?" taking two Aldor  
entities and computing whether or not they are type-equivalent in the  
sense you presented in your last mail. What problem can you solve with it?

Kind regards,
Christian