[Axiom-developer] aldor type satisfacton

[Page, Bill]

Ralf,

> 
> On March 13, 2006 8:34 AM Ralf Hemmecke wrote:
> ... 
> >
> >  aldor -laldor -grun dirprod.as
> >  2 has 2: T
> >  2 has 3: T
> >
> > it can be understood with my previous explanation.
> 

On Monday, March 13, 2006 10:50 AM I wrote:
> I don't know what semantics to associate with the use of a
> member of some domain on the right-hand side of 'has'. In
> Axiom I only see
> 
>   if <domain> has <category>
> 
> In the Aldor documentation I have read a discussion of how a
> domain is said to "satisfy" a category, but I do not know how
> to apply this in your example above.
>

I am sorry, please ignore the above comment. I was confused by
the fact that you did not provide the code for "dirprod.as" in
your email. I presume that it was meant to be analogous to the
output ""true+false" of "dirprod.spad":

  foo(): OutputForm ==
     b2: Boolean := (DirProd(2, Integer) has _
       DirProdCat(2, Integer))
     b3: Boolean := (DirProd(2, Integer) has _
       DirProdCat(3, Integer))
     (b2::OutputForm) + (b3::OutputForm)

Section 7.7 of the Aldor User's Guide defines how type satisfaction
is supposed to work. In fact Axiom seems to implement most of this.
The only exception I found was the use of ().

Reviewing 7.7, I think the result from the current implementation
of Aldor is wrong according to it's own documentation. :(

> > If you look at DirProdCat as a function then clearly
> >   DirProdCat(2,Z) = DirProd(3,Z) = with{first:%->Z}
> > so why would one want another output?
> >
> > ----------- dirprod.as
> > #include "aldor"
> > #include "aldorio"
> >
> > define DirProdCat(n: Integer, R: Type): Category == with {
> >    first: % -> R;
> > }
> 
> Well, clearly the application of the category 'DIRPCAT(2,INT'
> makes good sense in Axiom, don't you think? How else would you
> propose to define this category? How could we do without it
> in defining the domain 'DIRPROD(2,INT)'? To me this is the
> reason why we want another output from your example Aldor
> program. I would conclude that in fact internally (as you
> already said above):
> 
>   DirProdCat(2,Z) ~= with{first:%->Z}
> 
> There must be something additional on the right-hand side
> that is not reflected in the syntax of the category constant
> 'with' clause.
> 

Refer specifically to section "7.5 Subtypes" of the Axiom Users
Guide:

"Note that Aldor is constructed so that a domain is only a
member of a named category if it explicitly inherits from the
category -- not if it merely exports the same collection of
(explicit) declarations."

-------------

So it seems clear to me that the fact that:

MyMonoid(T: Type, m: (T, T) -> T): Category == with {
    square: %-> %;
    default {
      Rep == T;
      square(t: %): % == per m(rep t, rep t)
    }
}

MyInteger1: Join(ArithmeticType,MyMonoid(Integer, *$Integer)) == Integer
add;
MyInteger2: ArithmeticType == Integer add;
extend MyInteger2: MyMonoid(MyInteger2, *$MyInteger2) == add;
...

macro {
     Z == Integer;
     M1 == MyInteger1;
     M2 == MyInteger2;
}
main(): () == {
   stdout << "1: " << (M1 has MyMonoid(Z, *$Z)) << newline;
   stdout << "2: " << (M1 has MyMonoid(Z, +$Z)) << newline;
   stdout << "3: " << (M2 has MyMonoid(M2, *$M2)) << newline;
   stdout << "4: " << (M2 has MyMonoid(M2, +$M2)) << newline;
}
main();
Returns:

1: T
2: T
3: T
4: T

------

is certainly incorrect. I expect:

1: T
2: F
3: T
4: F

Regards,
Bill Page.