Re: [Axiom-developer] "has" and "with"

[Ralf Hemmecke]

> | >        Now the compiler goes on typecheking the defnition x ** n.
> | >        It sees the use of expt() and find out that the only expt() in
> | >        scope if the one from RepeatedSquare(S).  Then it tries
> | >        to instantiate that package -- just like a function call.
> | >        From there, it applies the usual rules:  Can I coerce S of
> | >        type Monad to the expected argument type of RepeatedSquare()?
> | >        They answer comes out as "no".  Hence the error.
> | 
> | Well, of course the answer should be "yes".
>
> It is not clear to me why the answer should *of course" be "yes".

We have

RepeatedSquaring(S): Exports == Implementation where
   S: SetCategory with
        "*":(%,%)->%
   Exports == with
     expt: (S,PositiveInteger) -> S
   Implementation == add ...

and furthermore

Monad(): Category == SetCategory with
      "*": (%,%) -> %
      ...
    add
      import RepeatedSquaring(%)
      x:% ** n:PositiveInteger == expt(x,n)
      rightPower(a,n) == ...
      leftPower(a,n) == ...


This should behave approximately like

---BEGIN aaa.as
#include "aldor"
macro SetCategory == PrimitiveType;
RepeatedSquaring(S: SetCategory with {*: (%,%)->%}): with {
        expt: (S, Integer) -> S;
} == add {
        expt(s: S, i: Integer): S == s; -- dummy implementation
}

Monad(): Category == SetCategory with {
        *: (%,%) -> %;
    default {
#if DoesntWork
        import from RepeatedSquaring(%);
        (x:%) ** (n:Integer): % == expt(x,n);
#else
        (x:%) ** (n:Integer): % == expt(x,n)$RepeatedSquaring(%);
#endif
    }
}
---END aaa.as

woodpecker:~/scratch>aldor -laldor aaa.as
woodpecker:~/scratch>aldor -laldor -DDoesntWork aaa.as
"aaa.as", line 14:         (x:%) ** (n:Integer): % == expt(x,n);
                   ...................................^
[L14 C36] #1 (Error) There are no suitable meanings for the operator `expt'.

Well. In fact, I would have liked that the Aldor compiler also works for 
the second case. Clearly "expt: (%, Integer) -> %" is in scope since it 
was just imported via the import statement. I consider that a bug in the 
Aldor compiler.

% as the argument of RepeatedSquaring stands for a domain of type 
Monad(). Such a domain obviously satisfies

  SetCategory with {*: (%,%)->%}

since Monad() has these exports (and more in the Axiom library case).

The compiler should check whether the type of % exports SetCategory. Yes 
it does, since Monad() exports it.

The compiler should check whether the type of % exports

  *: (%,%)->%

. Yes it does, since Monad() exports it.

Now why I believe that the SPAD compiler returns "false" is the following.

SPAD does not have "default". Implementations of a category are 
implemented by a private domain (therefore the "add" instead of 
"default" in SPAD). Now if I take the definition of the AUG about what 
the type of "add {...}" is, then, of course the % in RepeatedSquaring of

    add
      import RepeatedSquaring(%)
      x:% ** n:PositiveInteger == expt(x,n)
      rightPower(a,n) == ...
      leftPower(a,n) == ...

(see naalgc.spad.pamphlet)
does *not* export

  *: (%,%)->%

and therefore the instantiation of RepeatedSquaring(%) must fail.

Gaby, you have given in

http://lists.nongnu.org/archive/html/axiom-developer/2007-08/msg00412.html

how the "add" part in the Monad definition is translated to a private 
domain. That looks perfectly fine to me.
Bill has already shown that a proper value for the argument of 
RepeatedSquaring as in

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

works fine.

Gaby, you write there:

       Now the compiler goes on typecheking the defnition x ** n.
       It sees the use of expt() and find out that the only expt() in
       scope if the one from RepeatedSquare(S).  Then it tries
       to instantiate that package -- just like a function call.
       From there, it applies the usual rules:  Can I coerce S of
       type Monad to the expected argument type of RepeatedSquare()?
       They answer comes out as "no".  Hence the error.

Why would the compiler want to "coerce" if all that is needed is to 
check whether S of type Monad has at least the exports that are required 
by the argument type of RepeatedSquaring. (And it has.) I don't see a 
need for coercion at all.

Ralf