[Axiom-developer] RE: [Aldor-l] exports and constants

[Bill Page]

Ralf,

On July 20, 2006 8:12 PM you wrote:
> 
> Thank you for your comments, but I don't seem to agree with 
> everything.

That is probably a good thing! :)

> 
> Let's keep this program since I'll refer to its output.
> 

Omitted for brevity. Please refer to:

http://wiki.axiom-developer.org/SandBoxAldorSemantics

> >>
> >> In particular, that "B has CatB" is a bit surprising, isn't it?
> 
> > I think you are dealing here with two separate but related
> > issues:
> > 1) *static* typing, and 2) inheritance rules. All types in Aldor
> > are static (or at least *nearly static*) meaning that they must
> > be resolved during the compilation phase.
> 
> The "B has CatB" result is not about static or dynamic. If you
> read the code above. Would you immediately be able to tell that
> the Type of B is NOT CatA (as "H: CatA" might suggest), but the
> same as the type of Dom?

You are right, this example has only to do with inheritance
(Other cases you mentioned involved static vs. dynamic types).

You say: "the Type of B is NOT CatA", ??? But what I see is that
the type of both B and H *is* CatA just as the code says it must
be if this program is going to compile (and it does)!

Perhaps your question really is: If B is of type CatA, how can it
also satisfy CatB? To understand this you must understand that
SomeCat is a subtype of both CatA and CatB and therefore a domain
that is a member of SomeCat is also a member of both CatA and CatB.

Refer especially to section 7.5 of the Aldor User's Guide:

  "Inheritance for domains from categories is analogous to class
  membership and inheritance between categories is analogous to
  class containment."

> 
> >> Has someone found a description in the Aldor UG of whether this
> >> is intended to be so or this should be considered a bug in the
> >> compiler?
> 
> > No, I don't think it is a bug. This is all rather well (although
> > perhaps too tersely explained in the Aldor Users Guide, under
> > the heading of "Type Satisfaction", see section 7.7.
> 
> I know that the html version of the user guide at aldor.org 
> is a little 
> different from the .pdf version, but it seems 7.7 and 7.8 are OK.
> Looking at the pdf version, I cannot find good explanations of what
> 
> H: CatA == Dom;
> 
> actually means.
> 
> The constant assignment
> 
> H == Dom;
> 
> is clear, though. H inherits type and value of Dom.

But this is very fundamental. H:CatA is a declaration of the type
of H. That is true no matter in what context this appears.

In Aldor := is an assignment and is processed at run-time, while
== is a definition and is processed by the compiler. See section 5.3
of the Users Guide:

  "The general syntax for a constant definition is:

      x : T == E

  x is an identifier giving the name of the constant.

  T is an expression giving the type of the constant. The type
  declaration is optional. If the type is declared, then the type
  of E must satisfy it. Otherwise the type is inferred from the
  type of the expression E."

> 
> >> There is a difference in the semantic, but I cannot
> >> remember that I have found a proper explanation of what
> >> "Ident: SomeType == Dom" actually means (no "add" here).
> 
> > In the above the value of 'Ident' *is* 'Dom' whereas in the
> > previous case 'Ident' is the name of a new domain whose
> > "parent domain" is 'Dom' - like the difference between
> 
> If Ident *is* Dom then what do you think the ": SomeType" is for?
> 
> >>>> One cannot, however write something like
> >>>>
> >>>> CatC: Category == with { }
> >>>> H: CatC == Dom;
> >>> Of Course not, because Dom does not provide CatC.
> >>>> Different from
> >>>>
> >>>> A: CatA == Dom add;
> >>>>
> >>>> the construct
> >>>>
> >>>> H: CatA == Dom;
> >>>>
> >>>> just means that H provides *at least* the exports of CatA, 
> >>>> and the compiler can tell, if Dom provides less.
> 
> > In the first case you are defining a new domain A which
> > satisfies only CatA. In the second case you are saying
> > that H is identical to Dom, but the compiler knows that
> > is not true.
> 
> First and second is not so clear to me now. Can you repeat your 
> statement. In particular I don't understand your last sentence.
> 
> >>> You can interpret both kinds as "provides at least".
> 
> > No, I don't think that is true.

As stated in section 5.3

  H: CatA == Dom

means that the type of Dom must satisfy CatA, i.e. 'Dom has CatA'
must be true, which is just another way to say that it "provides
*at least* the exports of CatA". Provided that the compiler can
determine that this is true, then H is a constant that denotes
exactly Dom.

On the other hand if we write

  A: CatA == Dom add

section 5.3 still applies. (So in that sense you are right.)

The difference is that now Dom is the parent domain of a new
domain: "which specifies a domain from which any or all of the
exports of the add can be inherited". (Ref: Section 7.8).

So 'Dom add' is a new domain which inherits from Dom, but now
we need to take into account the rule about the "Visibility of
inherited operations":

  "whenever an expression 'A add B' appears in a context requiring
  a domain whose type is the category C, then any operations
  required by C which are not defined in B are taken from the
  domain A.

So here the expression 'Dom add' appears in a context requiring a
domain whose type is CatA, so all operations (and by implication,
*only* those operations) required by CatA are taken from Dom.

> ...
> Bill Page wrote:
>> The reason of course is because the expression 'odd? random()'
>> is not static - it does not have a well-defined value at the
>> time that the source is compiled. It is only later when the
>> code is run that we can know if the condition is true or false
>> in a particular instance. The Aldor compiler is not able to
>> compile *types* of this kind.
> 
> Bill you should have tried the following piece of code.
> 
> ---BEGIN aaa5.as
> #include "aldor"
> define CatA: Category == with;
> define CatB: Category == with;
> define CatX: Category == with;
> 
> A: Join(CatX, CatA) == add;
> B: Join(CatX, CatB) == add;
> #if ADD
> import from MachineInteger;
> X: CatX == if odd? random(10) then (A add) else (B add);
> #else
> X: CatX == if true then A else B;
> #endif
> ---END aaa5.as
> 
>  >aldor -fx -laldor -DADD aaa5.as
> 
> compiles without any complaints. Now try without the ADD assertion.
> 
>  >aldor -fx -laldor aaa5.as
> "aaa5.as", line 14: X: CatX == if true then A else B;
>                      ...........^
> [L14 C12] #1 (Error) Have determined 0 possible types for the 
> expression.
>    Subexpression `A':
>       Meaning 1:
>                  Join(CatX, CatA) with
>                      ==...
>    Subexpression `B':
>       Meaning 1:
>                  Join(CatX, CatB) with
>                      ==...
>    The context requires an expression of type CatX.
> 
> 
> Are you now a bit more puzzled?

No. That makes perfectly good sense according to the Aldor Users
Guide. You can compile:

  define CatA: Category == with;
  define CatB: Category == with;
  define CatX: Category == with {CatA; CatB;}
  A: Join(CatX, CatA) == add;
  B: Join(CatX, CatB) == add;
  import from Integer;
  X: CatX == if odd? random(10) then A else B;

Maybe it is surprising that the compiler does not complain about

> X: CatX == if odd? random(10) then (A add) else (B add);

but then both A and B satisfy CatX in a vacuous sense: none of
these categories have any exports and so X is still a constant.

But suppose we try a little harder:

  import from Integer;
  define CatA: Category == with {n:Integer};
  define CatB: Category == with {n:Integer};
  define CatX: Category == with {n:Integer};
  A: Join(CatX, CatA) == add { n:Integer==1 };
  B: Join(CatX, CatB) == add { n:Integer==2 };
  X: CatX == if odd? random(10) then (A add) else (B add);

where n is a "category-valued constant" as described in section
7.9. Again (surprise!) Aldor compiles this with no errors. But
what output do we expect? Will evaluating n$X yield different
results each time it is called?

What we see at runtime in fact is that n$X is a constant just
as required. See the example at

http://wiki.axiom-developer.org/SandBoxAldorSemantics

Should we conclude that it is the compiler that evaluates the
expression 'odd? random(10)' at compile time? Or perhaps that
fact that n must be a constant is resolved in some other way?

> 
> Random things are not the problem. Obviously "A" and "A add" are
> not (treated) identical by the compiler.

I agree that "A" and "A add" are not treated identically but the
difference is more subtle then your example implies.

> ... 
> And to make you even more happy...
> 
> ---BEGIN aaa6.as
> #include "aldor"
> #include "aldorio"
> macro I == MachineInteger;
> define CatX: Category == with {foo: () -> I}
> A: CatX == add {foo(): I == 0;}
> B: CatX == add {foo(): I == 1;}
> 
> import from MachineInteger;
> X: CatX == if odd? random(10) then A else B;
> 
> main(): () == {
>       import from X;
>       stdout << foo() << newline;
> }
> main();
> ---END aaa6.as
> 
> woodpecker:~>aldor -fx -laldor aaa6.as
> woodpecker:~>aaa6
> 0
> woodpecker:~>aaa6
> 0
> woodpecker:~>aaa6
> 0
> woodpecker:~>aaa6
> 0
> woodpecker:~>aaa6
> 0
> woodpecker:~>aaa6
> 1
> woodpecker:~>aaa6
> 1
> 
> It's only the type of X that must be clear at compile time.

I agree that it is the type of X must be clear. But something
very strange is going on here. I do not get this result in my
example running Aldor inside Axiom. See again:

http://wiki.axiom-developer.org/SandBoxAldorSemantics

If you write:

  main(): () == {
        import from X;
        stdout << foo() << newline;
        stdout << foo() << newline;
        stdout << foo() << newline;
        stdout << foo() << newline;
        stdout << foo() << newline;
        stdout << foo() << newline;
  }
  main();

You will see that each time you run the program you will only
get one *constant* result (all 0's or all 1's). But if you run
the same program repeatedly (as you did above), then sometimes
you get one result and sometimes the other! Within a given
runtime of the program, the result is constant and not variable
as you might be expecting.

My conclusion is that Aldor must be sort of "faking" the
compilation of the constants in the sense that they are not
fully resolved at compile-time, yet they are indeed constant
within any run of the program. There must be some kind of
dynamic initialization phase at the start of the program.

> But maybe even that is just a current restriction of the compiler. 
> Categories are first class values and they should be computable
> at runtime.

I do not know of any examples where categories are computed at
runtime in Aldor except in the case of dependent types where
static type checking is still possible.
 
> But I won't go into detail since there are certain problems that
> occur if categories are truly "first class".

The devil is in the details and that is what we are discussing!
:)

> ... 
> >> ---BEGIN aaa2.as
> >> #include "aldor"
> >> import from String, TextWriter, Character;
> >>
> >> define CatA: Category == with;
> >> define CatB: Category == with;
> >> define CatX: Category == with;
> >>
> >> A: CatX with { CatA } == add;
> >> B: CatX with { CatB } == add;
> >>
> >> X: CatX == if true then (A add) else (B add); -- (*)
> >>
> >> stdout << "X has CatA: " << ( X has CatA ) << newline;
> >> stdout << "X has CatB: " << ( X has CatB ) << newline;
> >> stdout << "X has CatX: " << ( X has CatX ) << newline;
> >> ---END aaa2.as
> >>
> >> aldor -grun -laldor aaa2.as
> >> X has CatA: F
> >> X has CatB: F
> >> X has CatX: T
> >>
> >> That is clear, but why does the compiler reject the program 
> >> without the "add" in line (*)?
> 
> > It is because the types of A and B are not a subtypes of CatX.
> > But X can be a member of CatX defined by (A add) or (B add).
> 
> I don't understand.
> A is of type Join(CatX, CatA) and you are saying that this is not a 
> subtype of CatX??? Similar for B.
>

No, in the above program A is not of type Join(CatX, CatA), it is
just CatX. And CatA does not satisfy CatX.

 
> >> ---BEGIN aaa3.as
> >> #include "aldor"
> >> import from String, TextWriter, Character, MachineInteger;
> >>
> >> define CatA: Category == with;
> >> define CatB: Category == with;
> >> define CatX: Category == with;
> >>
> >> A: Join(CatX, CatA) == add;
> >> B: Join(CatX, CatB) == add;
> >>
> >> MyPkg(X: CatX): with {isA?: () -> Boolean} == add {
> >>    isA?(): Boolean == X has CatA;
> >> }
> >> main(): () == {
> >>    import from CommandLine, Array String;
> >>    X: CatX == if zero? #arguments then (A add) else (B add);
> >>    stdout << isA?()$MyPkg(X) << zero? #arguments << newline;
> >> }
> >> main();
> >> ---END aaa3.as
> >>
> >>  >aldor -fx -laldor aaa3.as
> >>  >aaa3
> >> FT
> >>  >aaa3 1
> >> FF
> 
> > Static type again: the value of 'isA()' is determined at
> > compile time and does not depend on #arguments.
> 
> That is completely wrong. If "isA?()" would be computed at 
> compile time, I would be really amazed. X is a parameter to
> MyPkg. How should the compiler be able to evaluate "X has CatA"
> at all?
>

X is a domain of type CatX, thus X has CatA is always false.

> ... 
> Maybe I don't quite understand your "static", but I believe 
> that what I have demonstrated above shows that Aldor just
> requires that types are constant in a certain context, but
> otherwise one can do quite a lot with them.

By "static" I just mean that in Aldor the type-correctness of a
program can be checked entirely at compile-time. Because Aldor's
type system is quite complex, including the possibility of
dependent types, then you are right that this does not mean
that all types in Aldor are constant. But so far I don't think
you have given an example where this is not the case.

> 
> My feeling is that categories are not really "first class" in
> Aldor (which is certainly another issue). I haven't seen any
> reasonable program that computes a category and then creates
> a domain that belongs to that category. That the compiler cannot
> handle computed categories, I can understand, but I don't even
> know whether it would be useful to treat categories as "first
> class citizens".
> 

I would look at the situation of dependent types.

Regards,
Bill Page.